vect2_cont_comp2[T1,T2: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
%
%  Note that rT, frT could be generalized to [T1 -> T2]
%  Perhaps this should be done in anotrher theory with importings T1,T2
%
%------------------------------------------------------------------------------
BEGIN 

  IMPORTING cont_vect2_real, 
            cont_real_vect2 



  fvT : VAR [Vect2->T1]
  ftt : VAR [T1->T2]
  frv : VAR [T2->Vect2]

  v: VAR Vect2
  x: VAR T1

  ;o(ftt,fvT)  : [Vect2->T2]  = LAMBDA (v): ftt(fvT(v))

  ;o(frv,ftt)  : [T1->Vect2]  = LAMBDA (x): frv(ftt(x))

  vT         : VAR { f:[Vect2->T1] | continuous_vr?(f) }
  tt         : VAR { f:[T1->T2] | continuous?(f) }
  rv         : VAR { f:[T2->Vect2] | continuous_rv?(f) }


  comp_tt_vt_cont : LEMMA
    continuous_vr?(tt o vT)

  comp_rv_tt_cont : LEMMA
    continuous_rv?(rv o tt)

END vect2_cont_comp2