let D be non empty set ; :: thesis: for s being FinSequence of D
for n, m being Nat st n + m <= len s holds
(s | n) ^ ((s /^ n) | m) = s | (n + m)
let s be FinSequence of D; :: thesis: for n, m being Nat st n + m <= len s holds
(s | n) ^ ((s /^ n) | m) = s | (n + m)
let n, m be Nat; :: thesis: ( n + m <= len s implies (s | n) ^ ((s /^ n) | m) = s | (n + m) )
assume A1: n + m <= len s ; :: thesis: (s | n) ^ ((s /^ n) | m) = s | (n + m)
set f0 = s /^ n;
A2: (s | n) ^ (s /^ n) = s by RFINSEQ:8;
set f1 = (s /^ n) | m;
set f2 = (s /^ n) /^ m;
set f3 = (s | n) ^ ((s /^ n) | m);
A3: (s | n) ^ (((s /^ n) | m) ^ ((s /^ n) /^ m)) = s by A2, RFINSEQ:8;
n <= n + m by NAT_1:11;
then n <= len s by A1, XXREAL_0:2;
then A4: ( len (s | n) = n & len (s /^ n) = (len s) - n ) by FINSEQ_1:59, RFINSEQ:def 1;
then n + m <= n + (len (s /^ n)) by A1;
then len ((s /^ n) | m) = m by FINSEQ_1:59, XREAL_1:6;
then len ((s | n) ^ ((s /^ n) | m)) = n + m by A4, FINSEQ_1:22;
then dom ((s | n) ^ ((s /^ n) | m)) = Seg (n + m) by FINSEQ_1:def 3;
hence (s | n) ^ ((s /^ n) | m) = (((s | n) ^ ((s /^ n) | m)) ^ ((s /^ n) /^ m)) | (Seg (n + m)) by FINSEQ_1:21
.= s | (n + m) by A3, FINSEQ_1:32 ;
:: thesis: verum