deffunc H₁( Element of NAT ) -> Element of K21(the carrier of (TOP-REAL 2)) = Upper_Arc (L~ (Cage C,$1));
thus for S1, S2 being SetSequence of the carrier of (TOP-REAL 2) st ( for i being Element of NAT holds S1 . i = H₁(i) ) & ( for i being Element of NAT holds S2 . i = H₁(i) ) holds
S1 = S2 from BINOP_2:sch 1(); :: thesis: verum