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 in NAT holds
BSeq . y = CSeq . y

proof

let y be object ; :: thesis: ( y in NAT implies BSeq . y = CSeq . y )
assume y in NAT ; :: thesis: BSeq . y = CSeq . y
then reconsider y = y as Nat ;
set Y = { (B . k) where k is Nat : y <= k } ;
BSeq . y = union { (B . k) where k is Nat : y <= k } by A2;
hence BSeq . y = CSeq . y by A3; :: thesis: verum

end;

hence BSeq = CSeq by A2, A3, FUNCT_1:2; :: thesis: verum