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

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

hence
BSeq = CSeq
by A2, A3, FUNCT_1:2; :: thesis: verum
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;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