deffunc H₁( Nat) -> Element of K16( the carrier of (TOP-REAL 2)) = Upper_Arc (L~ (Cage (C,$1)));
consider S being SetSequence of the carrier of (TOP-REAL 2) such that
A1: for i being Element of NAT holds S . i = H₁(i) from FUNCT_2:sch 4();
take S ; :: thesis: for i being Nat holds S . i = Upper_Arc (L~ (Cage (C,i)))
let i be Nat; :: thesis: S . i = Upper_Arc (L~ (Cage (C,i)))
i in NAT by ORDINAL1:def 12;
hence S . i = Upper_Arc (L~ (Cage (C,i))) by A1; :: thesis: verum