let f, g be XFinSequence; :: thesis: mid (f ^ g),((len f) + 1),((len f) + (len g)) = g
A2: mid (f ^ g),((len f) + 1),((len f) + (len g)) = ((f ^ g) | ((len f) + (len g))) /^ (((len f) + 1) -' 1) by AB540b;
A3: ((len f) + 1) -' 1 = len f by NAT_D:34;
len (f ^ g) = (len f) + (len g) by AFINSQ_1:20;
then (f ^ g) | ((len f) + (len g)) = f ^ g by Lm4;
hence mid (f ^ g),((len f) + 1),((len f) + (len g)) = g by Th40, A2, A3; :: thesis: verum