let BSeq, CSeq be Function; :: thesis: ( dom BSeq =NAT & ( for n being Nat holds BSeq . n =union { (B . k) where k is Nat : n <= k } ) & dom CSeq =NAT & ( for n being Nat holds CSeq . n =union { (B . k) where k is Nat : n <= k } ) implies BSeq = CSeq ) assume that A2:
( dom BSeq =NAT & ( for n being Nat holds BSeq . n =union { (B . k) where k is Nat : n <= k } ) )
and A3:
( dom CSeq =NAT & ( for m being Nat holds CSeq . m =union { (B . k) where k is Nat : m <= k } ) )
; :: thesis: BSeq = CSeq
for y being object st y inNAT holds BSeq . y = CSeq . y