let s1, s2 be SetSequence of the carrier of (TOP-REAL 2); :: thesis: ( ( for i being Nat holds s1 . i = Upper_Arc (L~ (Cage (C,i))) ) & ( for i being Nat holds s2 . i = Upper_Arc (L~ (Cage (C,i))) ) implies s1 = s2 )

assume that

A2: for i being Nat holds s1 . i = Upper_Arc (L~ (Cage (C,i))) and

A3: for i being Nat holds s2 . i = Upper_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 = Upper_Arc (L~ (Cage (C,i))) by A2

.= s2 . i by A3 ; :: thesis: verum

assume that

A2: for i being Nat holds s1 . i = Upper_Arc (L~ (Cage (C,i))) and

A3: for i being Nat holds s2 . i = Upper_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 = Upper_Arc (L~ (Cage (C,i))) by A2

.= s2 . i by A3 ; :: thesis: verum