let D be set ; :: thesis: for p being XFinSequence of D holds FS2XFS (XFS2FS p) = p
let p be XFinSequence of D; :: thesis: FS2XFS (XFS2FS p) = p
A1: len p = len (XFS2FS p) by Def9A;
A2: len (XFS2FS p) = len (FS2XFS (XFS2FS p)) by Def8;
for k being Nat st k < len p holds
p . k = (FS2XFS (XFS2FS p)) . k

proof

let k be Nat; :: thesis: ( k < len p implies p . k = (FS2XFS (XFS2FS p)) . k )
assume A3: k < len p ; :: thesis: p . k = (FS2XFS (XFS2FS p)) . k
then ( 0 + 1 <= k + 1 & k + 1 < (len p) + 1 ) by XREAL_1:6;
then A4: ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:13;
thus p . k = p . ((k + 1) - 1)
.= (XFS2FS p) . (k + 1) by A4, Def9A
.= (FS2XFS (XFS2FS p)) . k by A1, A3, Def8 ; :: thesis: verum

end;

hence FS2XFS (XFS2FS p) = p by A1, A2, Th8; :: thesis: verum