let f, g be XFinSequence; :: thesis: mid (f ^ g),((len f) + 1),((len f) + (len g)) = g
A1: ((len f) + 1) -' 1 = len f by NAT_D:34;
len (f ^ g) = (len f) + (len g) by AFINSQ_1:20;
then A2: (f ^ g) | ((len f) + (len g)) = f ^ g by Th10;
mid (f ^ g),((len f) + 1),((len f) + (len g)) = ((f ^ g) | ((len f) + (len g))) /^ (((len f) + 1) -' 1) by Def3;
hence mid (f ^ g),((len f) + 1),((len f) + (len g)) = g by A1, A2, Th21; :: thesis: verum