let D be non empty set ; :: thesis: for d1, d2 being XFinSequence of D st XFS2FS d1 = XFS2FS d2 holds
d1 = d2
let d1, d2 be XFinSequence of D; :: thesis: ( XFS2FS d1 = XFS2FS d2 implies d1 = d2 )
assume A1: XFS2FS d1 = XFS2FS d2 ; :: thesis: d1 = d2
set Xd1 = XFS2FS d1;
set Xd2 = XFS2FS d2;
A2: len (XFS2FS d1) = len d1 by AFINSQ_1:def 9;
A3: len (XFS2FS d2) = len d2 by AFINSQ_1:def 9;
for i being Nat st i < len d1 holds
d1 . i = d2 . i

proof

let i be Nat; :: thesis: ( i < len d1 implies d1 . i = d2 . i )
assume A4: i < len d1 ; :: thesis: d1 . i = d2 . i
A5: i + 1 <= len d1 by A4, NAT_1:13;
A6: (i + 1) - 1 = i ;
then d1 . i = (XFS2FS d1) . (i + 1) by NAT_1:11, A5, AFINSQ_1:def 9;
hence d1 . i = d2 . i by A6, NAT_1:11, A5, A2, A3, A1, AFINSQ_1:def 9; :: thesis: verum

end;

hence d1 = d2 by A2, A3, A1, AFINSQ_1:9; :: thesis: verum