let BSeq, CSeq be Function; :: thesis: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = meet { (B . k) where k is Element of NAT : n <= k } ) & dom CSeq = NAT & ( for n being Element of NAT holds CSeq . n = meet { (B . k) where k is Element of NAT : n <= k } ) implies BSeq = CSeq )
assume that
A1: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = meet { (B . k) where k is Element of NAT : n <= k } ) ) and
A2: ( dom CSeq = NAT & ( for m being Element of NAT holds CSeq . m = meet { (B . k) where k is Element of NAT : m <= k } ) ) ; :: thesis: BSeq = CSeq
for y being set st y in NAT holds
BSeq . y = CSeq . y

proof

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

end;

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