vect_deriv_2D [ T : TYPE FROM real ] : THEORY
BEGIN
  ASSUMING
      IMPORTING analysis@deriv_domain_def

     deriv_domain      : ASSUMPTION deriv_domain?[T]

     not_one_element  : ASSUMPTION not_one_element?[T]

  ENDASSUMING

  IMPORTING deriv_real_vect2[T]

  s   : VAR Vect2
  a,r: VAR T

  V : VAR (derivable_rv?)

  detsv(s,V)(r): real =
    det(s,V(r))

  detsv_diff : LEMMA
    derivable?(detsv(s,V))

  detsvp_deriv : LEMMA
    deriv(detsv(s,V))(r) = det(s,deriv_rv(V)(r))

  sqvdot_diff : LEMMA
    derivable?(LAMBDA(r):sqv(V(r)))

  sqvdot_deriv : LEMMA
    deriv(LAMBDA(r):sqv(V(r)))(r) = 2*V(r)*deriv_rv(V)(r)

END vect_deriv_2D