let p, q be XFinSequence; :: thesis: mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q
A1: ((len p) + 1) -' 1 = len p by NAT_D:34;
len (p ^ q) = (len p) + (len q) by AFINSQ_1:17;
hence mid ((p ^ q),((len p) + 1),((len p) + (len q))) = q by A1, Th12; :: thesis: verum