let BSeq, CSeq be SetSequence of X; :: thesis: ( ( for n being Nat holds BSeq . n = (A1 . n) ` ) & ( for n being Nat holds CSeq . n = (A1 . n) ` ) implies BSeq = CSeq )
assume that
A3: for n being Nat holds BSeq . n = (A1 . n) ` and
A4: for m being Nat holds CSeq . m = (A1 . m) ` ; :: thesis: BSeq = CSeq
A5: for x being object st x in NAT holds
BSeq . x = CSeq . x
proof
let x be object ; :: thesis: ( x in NAT implies BSeq . x = CSeq . x )
assume x in NAT ; :: thesis: BSeq . x = CSeq . x
then reconsider x = x as Element of NAT ;
BSeq . x = (A1 . x) ` by A3
.= CSeq . x by A4 ;
hence BSeq . x = CSeq . x ; :: thesis: verum
end;
thus BSeq = CSeq by A5; :: thesis: verum