let n, k 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

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 Def4;
then k >= len q by A1, XREAL_1:10;
then dom q c= k by NAT_1:40;
then A3: q | k = q by RELAT_1:97;
dom (p ^ q) c= n by A2, NAT_1:40;
hence (p ^ q) | n = p ^ (q | k) by A3, RELAT_1:97; :: thesis: verum

end;

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

then A5: len ((p ^ q) | n) = n by Th13;
n < (len p) + (len q) by A4, Def4;
then k < len q by A1, XREAL_1:8;
then len (q | k) = k by Th13;
then A6: len (p ^ (q | k)) = (len p) + k by Def4;

now

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
B1: m < len ((p ^ q) | n) by A7, NAT_1:45;
then m < len (p ^ q) by A4, A5, XXREAL_0:2;
then A8: m in len (p ^ q) by NAT_1:45;
m in n by A4, Th13, A7;
then A9: m in (dom (p ^ q)) /\ n by A8, XBOOLE_0:def 4;
then A10: ((p ^ q) | n) . m = (p ^ q) . m by FUNCT_1:71;

now

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

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

then m in dom p by NAT_1:45;
then ( (p ^ (q | k)) . m = p . m & (p ^ q) . m = p . m ) by Def4;
hence ((p ^ q) | n) . m = (p ^ (q | k)) . m by A9, FUNCT_1:71; :: thesis: verum

end;

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

m < len (p ^ q) by A4, A5, XXREAL_0:2, B1;
then A12: q . (m - (len p)) = (p ^ q) . m by A11, Th22;
A13: (m - (len p)) + (len p) < len (p ^ q) by A4, A5, XXREAL_0:2, B1;
A14: m - (len p) is Nat by A11, NAT_1:21;
len (p ^ q) = (len p) + (len q) by Def4;
then m - (len p) < len q by A13, XREAL_1:8;
then A15: m - (len p) in len q by A14, NAT_1:45;
m - (len p) < k by A1, A5, A13, XREAL_1:8, B1;
then m - (len p) in k by A14, NAT_1:45;
then A16: m - (len p) in k /\ (dom q) by A15, XBOOLE_0:def 4;
(p ^ (q | k)) . m = (q | k) . (m - (len p)) by A1, A6, A5, A11, B1, Th22;
hence ((p ^ q) | n) . m = (p ^ (q | k)) . m by A10, A12, A16, FUNCT_1:71; :: 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 Th10, A6, A1, A4, Th13; :: thesis: verum

end;

end;

end;

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