deffunc H₁( Element of NAT ) -> Element of K6( the carrier of (TOP-REAL 2)) = Lower_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