let D be non empty set ; :: thesis: for d being XFinSequence of D
for n being Nat holds XFS2FS (d | n) = (XFS2FS d) | n
let d be XFinSequence of D; :: thesis: for n being Nat holds XFS2FS (d | n) = (XFS2FS d) | n
let n be Nat; :: thesis: XFS2FS (d | n) = (XFS2FS d) | n
set di = d | n;
set Xd = XFS2FS d;
set Xdi = XFS2FS (d | n);
A1: len (XFS2FS d) = len d by AFINSQ_1:def 9;
A2: len (XFS2FS (d | n)) = len (d | n) by AFINSQ_1:def 9;

per cases ( n >= len d or n <= len d ) ;

suppose A3: n >= len d ; :: thesis: XFS2FS (d | n) = (XFS2FS d) | n

then d | n = d by AFINSQ_1:52;
hence XFS2FS (d | n) = (XFS2FS d) | n by A3, A1, FINSEQ_1:58; :: thesis: verum

end;

suppose A4: n <= len d ; :: thesis: XFS2FS (d | n) = (XFS2FS d) | n

then A5: len (d | n) = n by AFINSQ_1:54;

now :: thesis: for k being Nat st 1 <= k & k <= n holds
(XFS2FS (d | n)) . k = ((XFS2FS d) | n) . k

let k be Nat; :: thesis: ( 1 <= k & k <= n implies (XFS2FS (d | n)) . k = ((XFS2FS d) | n) . k )
assume that
A6: 1 <= k and
A7: k <= n ; :: thesis: (XFS2FS (d | n)) . k = ((XFS2FS d) | n) . k
k -' 1 = k - 1 by A6, XREAL_1:48, XREAL_0:def 2;
then (k -' 1) + 1 = k ;
then k -' 1 < n by A7, NAT_1:13;
then A8: card (Segm (k -' 1)) in card (Segm n) by NAT_1:41;
A9: k <= len d by A4, A7, XXREAL_0:2;
thus (XFS2FS (d | n)) . k = (d | n) . (k -' 1) by A6, A7, A5, AFINSQ_1:def 9
.= d . (k -' 1) by A8, A4, AFINSQ_1:53
.= (XFS2FS d) . k by A9, A6, AFINSQ_1:def 9
.= ((XFS2FS d) | n) . k by A7, FINSEQ_3:112 ; :: thesis: verum

end;

hence XFS2FS (d | n) = (XFS2FS d) | n by A5, A4, A1, FINSEQ_1:59, A2; :: thesis: verum

end;

end;