let n be Element of NAT ; :: thesis: for p' being XFinSequence ex q' being XFinSequence st p' = (p' | n) ^ q'
let p' be XFinSequence; :: thesis: ex q' being XFinSequence st p' = (p' | n) ^ q'

now

per cases ( n > len p' or n <= len p' ) ;

suppose n > len p' ; :: thesis: ex q' being XFinSequence st p' = (p' | n) ^ q'

then ( len p' c= n & dom p' = len p' ) by NAT_1:40;
then ( p' | n = p' & p' ^ {} = p' & {} is XFinSequence ) by AFINSQ_1:32, RELAT_1:97;
hence ex q' being XFinSequence st p' = (p' | n) ^ q' ; :: thesis: verum

end;

suppose A1: n <= len p' ; :: thesis: ex q' being XFinSequence st p' = (p' | n) ^ q'

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: S₁[ 0 ]

proof

( p' | ((len p') - 0 ) = p' & p' ^ {} = p' & {} is XFinSequence ) by AFINSQ_1:32, RELAT_1:97;
hence S₁[ 0 ] ; :: thesis: verum

end;

A3: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

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

end;

A7: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A2, A3);
reconsider n1 = (len p') - n as Element of NAT by A1, NAT_1:21;
reconsider n2 = (len p') - n1 as Element of NAT ;
ex q' being XFinSequence st p' = (p' | n2) ^ q' by A7;
hence ex q' being XFinSequence st p' = (p' | n) ^ q' ; :: thesis: verum

end;

end;

end;

hence ex q' being XFinSequence st p' = (p' | n) ^ q' ; :: thesis: verum