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