let BSeq, CSeq be SetSequence of X; :: thesis: ( ( for n being Element of NAT holds BSeq . n = (A1 . n) ` ) & ( for n being Element of NAT holds CSeq . n = (A1 . n) ` ) implies BSeq = CSeq )
assume that
A1: for n being Element of NAT holds BSeq . n = (A1 . n) ` and
A2: for m being Element of NAT holds CSeq . m = (A1 . m) ` ; :: thesis: BSeq = CSeq
A3: for x being set st x in NAT holds
BSeq . x = CSeq . x

proof

let x be set ; :: 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 A1
.= CSeq . x by A2 ;
hence BSeq . x = CSeq . x ; :: thesis: verum

end;

( NAT = dom BSeq & NAT = dom CSeq ) by FUNCT_2:def 1;
hence BSeq = CSeq by A3, FUNCT_1:9; :: thesis: verum