end;

then reconsider n1 = (len p') - n as Element of NAT by NAT_1:21;
defpred S₁[ Nat] means for k being Element of NAT st k = (len p') - $1 holds
ex q' being XFinSequence st p' = (p' | k) ^ q';
A2: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

let m be Element of NAT ; :: thesis:
assume A3: S₁[m] ; :: thesis:
let k be Element of NAT ; :: thesis:
assume A4: k = (len p') - (m + 1) ; :: thesis:
consider q' being XFinSequence such that
A5: p' = (p' | (k + 1)) ^ q' by A3, A4;
k <= k + 1 by NAT_1:11;
then k c= k + 1 by NAT_1:40;
then A6: (p' | (k + 1)) | k = p' | k by RELAT_1:103;
A7: p' | (k + 1) is XFinSequence of rng (p' | (k + 1)) by RELAT_1:def 19;
(len p') - m <= (len p') - 0 by XREAL_1:12;
then ( ( k + 1 = len p' & dom (p' | (len p')) = len p' ) or k + 1 < len p' ) by A4, RELAT_1:97, XXREAL_0:1;
then A8: len (p' | (k + 1)) = k + 1 by AFINSQ_1:14;
then rng (p' | (k + 1)) <> {} by RELAT_1:65;
then p' | (k + 1) = ((p' | (k + 1)) | k) ^ <%((p' | (k + 1)) . k)%> by A8, A7, CARD_FIN:43;
then p' = (p' | k) ^ (<%((p' | (k + 1)) . k)%> ^ q') by A5, A6, AFINSQ_1:30;
hence ex q' being XFinSequence st p' = (p' | k) ^ q' ; :: thesis:

end;

end;