let n, k be Element of 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 AFINSQ_1:20;
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 AFINSQ_1:14;
n < (len p') + (len q') by A4, AFINSQ_1:20;
then k < len q' by A1, XREAL_1:8;
then len (q' | k) = k by AFINSQ_1:14;
then A6: len (p' ^ (q' | k)) = (len p') + k by AFINSQ_1:20;

now

let m be Element of NAT ; :: thesis: ( m < len ((p' ^ q') | n) implies ((p' ^ q') | n) . m = (p' ^ (q' | k)) . m )
assume A7: m < len ((p' ^ q') | n) ; :: thesis: ((p' ^ q') | n) . m = (p' ^ (q' | k)) . m
m < len (p' ^ q') by A4, A5, A7, XXREAL_0:2;
then A8: m in len (p' ^ q') by NAT_1:45;
m in n by A5, A7, NAT_1:45;
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 AFINSQ_1:def 4;
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, A7, XXREAL_0:2;
then A12: q' . (m - (len p')) = (p' ^ q') . m by A11, AFINSQ_1:22;
A13: (m - (len p')) + (len p') < len (p' ^ q') by A4, A5, A7, XXREAL_0:2;
A14: m - (len p') is Nat by A11, NAT_1:21;
len (p' ^ q') = (len p') + (len q') by AFINSQ_1:20;
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, A7, A13, XREAL_1:8;
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, A7, A11, AFINSQ_1:22;
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 A1, A4, A6, AFINSQ_1:11, AFINSQ_1:14; :: thesis: verum

end;

end;

end;

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