let k, n be Nat; :: thesis: for p, q being XFinSequence st n = (dom p) + k holds
(p ^ q) | n = p ^ (q | k)
let p, q be XFinSequence; :: thesis: ( n = (dom p) + k implies (p ^ q) | n = p ^ (q | k) )
assume A1: n = (dom p) + k ; :: thesis: (p ^ q) | n = p ^ (q | k)

now :: thesis: (p ^ q) | n = p ^ (q | k)

per cases ( n >= len (p ^ q) or n < len (p ^ q) ) ;

suppose A2: n >= len (p ^ q) ; :: thesis: (p ^ q) | n = p ^ (q | k)

then n >= (len p) + (len q) by Def3;
then Segm (len q) c= Segm k by NAT_1:39, A1, XREAL_1:8;
then A3: q | k = q by RELAT_1:68;
Segm (len (p ^ q)) c= Segm n by A2, NAT_1:39;
hence (p ^ q) | n = p ^ (q | k) by A3, RELAT_1:68; :: thesis: verum

end;

suppose A4: n < len (p ^ q) ; :: thesis: (p ^ q) | n = p ^ (q | k)

then A5: len ((p ^ q) | n) = n by Th10;
n < (len p) + (len q) by A4, Def3;
then k < len q by A1, XREAL_1:6;
then len (q | k) = k by Th10;
then A6: len (p ^ (q | k)) = (len p) + k by Def3;

now :: thesis: for m being Nat st m in dom ((p ^ q) | n) holds
((p ^ q) | n) . m = (p ^ (q | k)) . m

let m be Nat; :: thesis: ( m in dom ((p ^ q) | n) implies ((p ^ q) | n) . m = (p ^ (q | k)) . m )
assume A7: m in dom ((p ^ q) | n) ; :: thesis: ((p ^ q) | n) . m = (p ^ (q | k)) . m
A8: m < len ((p ^ q) | n) by A7, Lm1;
then m < len (p ^ q) by A4, A5, XXREAL_0:2;
then A9: m in len (p ^ q) by Lm1;
m in n by A4, Th10, A7;
then A10: m in (dom (p ^ q)) /\ n by A9, XBOOLE_0:def 4;
then A11: ((p ^ q) | n) . m = (p ^ q) . m by FUNCT_1:48;

now :: thesis: ((p ^ q) | n) . m = (p ^ (q | k)) . m

per cases ( m < len p or m >= len p ) ;

suppose m < len p ; :: thesis: ((p ^ q) | n) . m = (p ^ (q | k)) . m

then m in dom p by Lm1;
then ( (p ^ (q | k)) . m = p . m & (p ^ q) . m = p . m ) by Def3;
hence ((p ^ q) | n) . m = (p ^ (q | k)) . m by A10, FUNCT_1:48; :: thesis: verum

end;

suppose A12: m >= len p ; :: thesis: ((p ^ q) | n) . m = (p ^ (q | k)) . m

m < len (p ^ q) by A4, A5, A8, XXREAL_0:2;
then A13: q . (m - (len p)) = (p ^ q) . m by A12, Th17;
A14: (m - (len p)) + (len p) < len (p ^ q) by A4, A5, A8, XXREAL_0:2;
A15: m - (len p) is Nat by A12, NAT_1:21;
len (p ^ q) = (len p) + (len q) by Def3;
then m - (len p) < len q by A14, XREAL_1:6;
then A16: m - (len p) in len q by A15, Lm1;
m - (len p) < k by A1, A5, A14, A8, XREAL_1:6;
then m - (len p) in Segm k by A15, NAT_1:44;
then A17: m - (len p) in k /\ (dom q) by A16, XBOOLE_0:def 4;
(p ^ (q | k)) . m = (q | k) . (m - (len p)) by A1, A6, A5, A12, A8, Th17;
hence ((p ^ q) | n) . m = (p ^ (q | k)) . m by A11, A13, A17, FUNCT_1:48; :: thesis: verum

end;

end;

end;

hence ((p ^ q) | n) . m = (p ^ (q | k)) . m ; :: thesis: verum

end;

hence (p ^ q) | n = p ^ (q | k) by A6, A1, A4, Th10; :: thesis: verum

end;

end;

end;

hence (p ^ q) | n = p ^ (q | k) ; :: thesis: verum