deffunc H_{1}( 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

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