let D be set ; :: thesis: for d being FinSequence of D holds XFS2FS (FS2XFS d) = d
let d be FinSequence of D; :: thesis: XFS2FS (FS2XFS d) = d
set Xd = FS2XFS d;
A1: len d = len (FS2XFS d) by AFINSQ_1:def 8;
A2: len (FS2XFS d) = len (XFS2FS (FS2XFS d)) by AFINSQ_1:def 9;
now :: thesis: for i being Nat st 1 <= i & i <= len d holds
d . i = (XFS2FS (FS2XFS d)) . i
let i be Nat; :: thesis: ( 1 <= i & i <= len d implies d . i = (XFS2FS (FS2XFS d)) . i )
assume that
A3: 1 <= i and
A4: i <= len d ; :: thesis: d . i = (XFS2FS (FS2XFS d)) . i
reconsider i1 = i - 1 as Nat by A3, NAT_1:21;
A5: i1 + 1 = i ;
A6: i -' 1 = i1 by XREAL_0:def 2;
thus d . i = (FS2XFS d) . i1 by A4, A5, NAT_1:13, AFINSQ_1:def 8
.= (XFS2FS (FS2XFS d)) . i by A3, A4, A6, A1, AFINSQ_1:def 9 ; :: thesis: verum
end;
hence XFS2FS (FS2XFS d) = d by A1, A2; :: thesis: verum