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

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

thus
BSeq = CSeq
by A5; :: thesis: verum
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;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