let k, n be Nat; 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; ( len p = n + k implies ex q1, q2 being XFinSequence st
( len q1 = n & len q2 = k & p = q1 ^ q2 ) )
defpred S1[ 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 for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A2:
S1[
n]
;
S1[n + 1]thus
S1[
n + 1]
verumproof
let p be
XFinSequence;
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;
( 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
;
ex q1, q2 being XFinSequence st
( len q1 = i & len q2 = j & p = q1 ^ q2 )
per cases
( j = 0 or j > 0 )
;
suppose
j > 0
;
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;
verum end; end;
end; end;
A13:
S1[ 0 ]
for n being Nat holds S1[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 ) )
; verum