let i, j be Nat; :: thesis: for p being XFinSequence st len p = i + j holds
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & 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: 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 A2: ( len p = 0 & len p = i + j ) ; :: thesis: ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
then A3: p = {} ;
A4: ( len {} = i & len {} = j ) by A2;
p = {} ^ {} by A3, AFINSQ_1:32;
hence ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) by A4; :: thesis: verum

end;

A5: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: 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 A7: ( len p = n + 1 & 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 A8: 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 A7, A8, AFINSQ_1:32; :: 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
A9: j = k + 1 by NAT_1:6;
A10: n = i + k by A7, A9;
p <> {} by A7;
then consider q being XFinSequence, x being set such that
A11: p = q ^ <%x%> by AFINSQ_1:44;
n + 1 = (len q) + (len <%x%>) by A7, A11, AFINSQ_1:20
.= (len q) + 1 by AFINSQ_1:36 ;
then consider q1, q2 being XFinSequence such that
A12: ( len q1 = i & len q2 = k & q = q1 ^ q2 ) by A6, A10;
A13: p = q1 ^ (q2 ^ <%x%>) by A11, A12, AFINSQ_1:30;
len (q2 ^ <%x%>) = (len q2) + (len <%x%>) by AFINSQ_1:20
.= j by A9, A12, AFINSQ_1:36 ;
hence ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 ) by A12, A13; :: thesis: verum

end;

end;

end;

end;

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