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

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len d1 implies (XFS2FS d1) . i = (XFS2FS d2) . i )
assume that
A3: 1 <= i and
A4: i <= len d1 ; :: thesis: (XFS2FS d1) . i = (XFS2FS d2) . i
(XFS2FS d1) . i = d1 . (i -' 1) by AFINSQ_1:def 9, A3, A4;
hence (XFS2FS d1) . i = (XFS2FS d2) . i by AFINSQ_1:def 9, A3, A4, A1; :: thesis: verum

end;

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