let D be set ; :: thesis: for p being XFinSequence of D
for n being Nat holds
( XFS2FS (p | n) = (XFS2FS p) | n & XFS2FS (p /^ n) = (XFS2FS p) /^ n )
let p be XFinSequence of D; :: thesis: for n being Nat holds
( XFS2FS (p | n) = (XFS2FS p) | n & XFS2FS (p /^ n) = (XFS2FS p) /^ n )
let n be Nat; :: thesis: ( XFS2FS (p | n) = (XFS2FS p) | n & XFS2FS (p /^ n) = (XFS2FS p) /^ n )
thus XFS2FS (p | n) = (XFS2FS p) | n :: thesis: XFS2FS (p /^ n) = (XFS2FS p) /^ n

proof

A1: now :: thesis: for x being object holds
( ( x in dom (XFS2FS (p | n)) implies x in dom ((XFS2FS p) | n) ) & ( x in dom ((XFS2FS p) | n) implies x in dom (XFS2FS (p | n)) ) )

let x be object ; :: thesis: ( ( x in dom (XFS2FS (p | n)) implies x in dom ((XFS2FS p) | n) ) & ( x in dom ((XFS2FS p) | n) implies x in dom (XFS2FS (p | n)) ) )

hereby :: thesis: ( x in dom ((XFS2FS p) | n) implies x in dom (XFS2FS (p | n)) )

assume A2: x in dom (XFS2FS (p | n)) ; :: thesis: x in dom ((XFS2FS p) | n)
then reconsider m1 = x as Nat ;
A3: ( 1 <= m1 & m1 <= len (XFS2FS (p | n)) ) by A2, FINSEQ_3:25;
then reconsider m = m1 - 1 as Nat by INT_1:74;
m + 1 in dom (XFS2FS (p | n)) by A2;
then m in dom (p | n) by AFINSQ_1:95;
then A4: ( m in dom p & m in n ) by RELAT_1:57;
then A5: m + 1 in dom (XFS2FS p) by AFINSQ_1:95;
m in Segm n by A4;
then m < n by NAT_1:44;
then m + 1 <= n by NAT_1:13;
then x in dom ((XFS2FS p) | (Seg n)) by A3, A5, FINSEQ_1:1, RELAT_1:57;
hence x in dom ((XFS2FS p) | n) by FINSEQ_1:def 16; :: thesis: verum

end;

assume x in dom ((XFS2FS p) | n) ; :: thesis: x in dom (XFS2FS (p | n))
then x in dom ((XFS2FS p) | (Seg n)) by FINSEQ_1:def 16;
then A6: ( x in dom (XFS2FS p) & x in Seg n ) by RELAT_1:57;
then reconsider m1 = x as Nat ;
A7: ( 1 <= m1 & m1 <= n ) by A6, FINSEQ_1:1;
then reconsider m = m1 - 1 as Nat by INT_1:74;
m + 1 in dom (XFS2FS p) by A6;
then A8: m in dom p by AFINSQ_1:95;
m + 1 <= n by A7;
then m < n by NAT_1:13;
then m in Segm n by NAT_1:44;
then m in dom (p | n) by A8, RELAT_1:57;
then m + 1 in dom (XFS2FS (p | n)) by AFINSQ_1:95;
hence x in dom (XFS2FS (p | n)) ; :: thesis: verum

end;

for k being Nat st k in dom (XFS2FS (p | n)) holds
(XFS2FS (p | n)) . k = ((XFS2FS p) | n) . k

proof

let k be Nat; :: thesis: ( k in dom (XFS2FS (p | n)) implies (XFS2FS (p | n)) . k = ((XFS2FS p) | n) . k )
assume A9: k in dom (XFS2FS (p | n)) ; :: thesis: (XFS2FS (p | n)) . k = ((XFS2FS p) | n) . k
then A10: ( 1 <= k & k <= len (XFS2FS (p | n)) ) by FINSEQ_3:25;
then reconsider m = k - 1 as Nat by INT_1:74;
m + 1 in dom (XFS2FS (p | n)) by A9;
then A11: m in dom (p | n) by AFINSQ_1:95;
then m in Segm (len (p | n)) ;
then m < len (p | n) by NAT_1:44;
then A12: m + 1 <= len (p | n) by NAT_1:13;
Segm (len (p | n)) c= Segm (len p) by RELAT_1:60;
then len (p | n) <= len p by NAT_1:39;
then A13: k <= len p by A12, XXREAL_0:2;
m in Segm n by A11;
then m < n by NAT_1:44;
then m + 1 <= n by NAT_1:13;
then A14: k in Seg n by A10, FINSEQ_1:1;
thus (XFS2FS (p | n)) . k = (p | n) . ((m + 1) - 1) by A10, A12, AFINSQ_1:def 9
.= (p | n) . m
.= p . m by A11, FUNCT_1:47
.= p . ((m + 1) - 1)
.= (XFS2FS p) . k by A10, A13, AFINSQ_1:def 9
.= ((XFS2FS p) | (Seg n)) . k by A14, FUNCT_1:49
.= ((XFS2FS p) | n) . k by FINSEQ_1:def 16 ; :: thesis: verum

end;

hence XFS2FS (p | n) = (XFS2FS p) | n by A1, TARSKI:2; :: thesis: verum

end;

per cases ( len p <= n or n < len p ) ;

suppose A15: len p <= n ; :: thesis: XFS2FS (p /^ n) = (XFS2FS p) /^ n

then p /^ n = {} by Th6;
then A16: XFS2FS (p /^ n) = {} ;
len ((XFS2FS p) /^ n) = 0

proof

per cases ( len p < n or len p = n ) by A15, XXREAL_0:1;

suppose len p < n ; :: thesis: len ((XFS2FS p) /^ n) = 0

then A17: (len p) - n < n - n by XREAL_1:14;
thus len ((XFS2FS p) /^ n) = (len (XFS2FS p)) -' n by RFINSEQ:29
.= (len p) -' n by AFINSQ_1:def 9
.= 0 by A17, XREAL_0:def 2 ; :: thesis: verum

end;

suppose A18: len p = n ; :: thesis: len ((XFS2FS p) /^ n) = 0

thus len ((XFS2FS p) /^ n) = (len (XFS2FS p)) -' n by RFINSEQ:29
.= (0 + (len p)) -' n by AFINSQ_1:def 9
.= 0 by A18, NAT_D:34 ; :: thesis: verum

end;

end;

end;

hence XFS2FS (p /^ n) = (XFS2FS p) /^ n by A16; :: thesis: verum

end;

suppose A19: n < len p ; :: thesis: XFS2FS (p /^ n) = (XFS2FS p) /^ n

then A20: n <= len (XFS2FS p) by AFINSQ_1:def 9;
A21: len (XFS2FS (p /^ n)) = len (p /^ n) by AFINSQ_1:def 9
.= (len p) -' n by Def2
.= (len (XFS2FS p)) -' n by AFINSQ_1:def 9
.= len ((XFS2FS p) /^ n) by RFINSEQ:29 ;

now :: thesis: for k being Nat st 1 <= k & k <= len (XFS2FS (p /^ n)) holds
(XFS2FS (p /^ n)) . k = ((XFS2FS p) /^ n) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (XFS2FS (p /^ n)) implies (XFS2FS (p /^ n)) . k = ((XFS2FS p) /^ n) . k )
assume A22: ( 1 <= k & k <= len (XFS2FS (p /^ n)) ) ; :: thesis: (XFS2FS (p /^ n)) . k = ((XFS2FS p) /^ n) . k
then A23: ( 1 <= k & k <= len (p /^ n) ) by AFINSQ_1:def 9;
then reconsider m = k - 1 as Nat by INT_1:74;
m + 1 <= len (p /^ n) by A23;
then m < len (p /^ n) by NAT_1:13;
then m in Segm (len (p /^ n)) by NAT_1:44;
then A24: m in dom (p /^ n) ;
A25: k in dom ((XFS2FS p) /^ n) by A21, A22, FINSEQ_3:25;
A26: 1 + 0 <= k + n by A23, XREAL_1:7;
k <= (len p) - n by A19, A23, Th7;
then A27: k + n <= ((len p) - n) + n by XREAL_1:6;
thus (XFS2FS (p /^ n)) . k = (p /^ n) . ((m + 1) - 1) by A23, AFINSQ_1:def 9
.= (p /^ n) . m
.= p . (m + n) by A24, Def2
.= p . (((n + m) + 1) - 1)
.= (XFS2FS p) . (k + n) by A26, A27, AFINSQ_1:def 9
.= ((XFS2FS p) /^ n) . k by A20, A25, RFINSEQ:def 1 ; :: thesis: verum

end;

hence XFS2FS (p /^ n) = (XFS2FS p) /^ n by A21; :: thesis: verum

end;

end;