deffunc H₁( Nat) -> Element of K16( the carrier of (TOP-REAL 2)) = Lower_Arc (L~ (Cage (C,$1)));
let s1, s2 be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Nat holds s1 . i = Lower_Arc (L~ (Cage (C,i))) ) & ( for i being Nat holds s2 . i = Lower_Arc (L~ (Cage (C,i))) ) implies s1 = s2 )
assume that
A5: for i being Nat holds s1 . i = Lower_Arc (L~ (Cage (C,i))) and
A6: for i being Nat holds s2 . i = Lower_Arc (L~ (Cage (C,i))) ; :: thesis: s1 = s2
let i be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: s1 . i = s2 . i
thus s1 . i = Lower_Arc (L~ (Cage (C,i))) by A5
.= s2 . i by A6 ; :: thesis: verum