deffunc H_{1}( Nat) -> Element of K16( the carrier of (TOP-REAL 2)) = Lower_Arc (L~ (Cage (C,$1)));

consider S being SetSequence of the carrier of (TOP-REAL 2) such that

A4: for i being Element of NAT holds S . i = H_{1}(i)
from FUNCT_2:sch 4();

take S ; :: thesis: for i being Nat holds S . i = Lower_Arc (L~ (Cage (C,i)))

let i be Nat; :: thesis: S . i = Lower_Arc (L~ (Cage (C,i)))

i in NAT by ORDINAL1:def 12;

hence S . i = Lower_Arc (L~ (Cage (C,i))) by A4; :: thesis: verum

consider S being SetSequence of the carrier of (TOP-REAL 2) such that

A4: for i being Element of NAT holds S . i = H

take S ; :: thesis: for i being Nat holds S . i = Lower_Arc (L~ (Cage (C,i)))

let i be Nat; :: thesis: S . i = Lower_Arc (L~ (Cage (C,i)))

i in NAT by ORDINAL1:def 12;

hence S . i = Lower_Arc (L~ (Cage (C,i))) by A4; :: thesis: verum