let k, n be Nat; :: thesis: for p being XFinSequence st len p = n + k holds
ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 )
let p be XFinSequence; :: thesis: ( len p = n + k implies ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 ) )
defpred S₁[ Nat] means for p being XFinSequence
for i, j being Nat st len p = $1 & len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 );

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let p be XFinSequence; :: thesis: for i, j being Nat st len p = n + 1 & len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
let i, j be Nat; :: thesis: ( len p = n + 1 & len p = i + j implies ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) )
assume that
A3: len p = n + 1 and
A4: len p = i + j ; :: thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )

per cases ( j = 0 or j > 0 ) ;

suppose A5: j = 0 ; :: thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )

take q1 = p; :: thesis: ex q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
take q2 = {} ; :: thesis: ( len q1 = i & len q2 = j & p = q1 ^ q2 )
thus ( len q1 = i & len q2 = j & p = q1 ^ q2 ) by A4, A5; :: thesis: verum

end;

suppose j > 0 ; :: thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )

then consider k being Nat such that
A6: j = k + 1 by NAT_1:6;
p <> {} by A3;
then consider q being XFinSequence, x being object such that
A7: p = q ^ <%x%> by Th37;
A8: n + 1 = (len q) + (len <%x%>) by A3, A7, Def3
.= (len q) + 1 by Th30 ;
n = i + k by A3, A4, A6;
then consider q1, q2 being XFinSequence such that
A9: len q1 = i and
A10: len q2 = k and
A11: q = q1 ^ q2 by A2, A8;
A12: len (q2 ^ <%x%>) = (len q2) + (len <%x%>) by Def3
.= j by A6, A10, Th30 ;
p = q1 ^ (q2 ^ <%x%>) by A7, A11, Th25;
hence ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) by A9, A12; :: thesis: verum

end;

end;

end;

end;

A13: S₁[ 0 ]

proof

let p be XFinSequence; :: thesis: for i, j being Nat st len p = 0 & len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
let i, j be Nat; :: thesis: ( len p = 0 & len p = i + j implies ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) )
assume that
A14: len p = 0 and
A15: len p = i + j ; :: thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
A16: p = {} ^ {} by A14;
len {} = i by A14, A15;
hence ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) by A15, A16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A1);
hence ( len p = n + k implies ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 ) ) ; :: thesis: verum