let p be FinSequence; :: thesis: ( p <> {} implies ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) )
defpred S₁[ Nat] means for p being FinSequence st p <> {} & len p = $1 holds
ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 );
assume A1: p <> {} ; :: thesis: ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 )

now :: thesis: for i being Nat st ( for p being FinSequence st p <> {} & len p = i holds
ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) ) holds
for p being FinSequence st p <> {} & len p = i + 1 holds
ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 )

let i be Nat; :: thesis: ( ( for p being FinSequence st p <> {} & len p = i holds
ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) ) implies for p being FinSequence st p <> {} & len p = i + 1 holds
ex x being object ex q being FinSequence st
( q = <*b₄*> ^ b₅ & len q = (len b₅) + 1 ) )
assume A2: for p being FinSequence st p <> {} & len p = i holds
ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) ; :: thesis: for p being FinSequence st p <> {} & len p = i + 1 holds
ex x being object ex q being FinSequence st
( q = <*b₄*> ^ b₅ & len q = (len b₅) + 1 )
let p be FinSequence; :: thesis: ( p <> {} & len p = i + 1 implies ex x being object ex q being FinSequence st
( q = <*b₃*> ^ b₄ & len q = (len b₄) + 1 ) )
assume that
A3: p <> {} and
A4: len p = i + 1 ; :: thesis: ex x being object ex q being FinSequence st
( q = <*b₃*> ^ b₄ & len q = (len b₄) + 1 )
consider q being FinSequence, y being object such that
A5: p = q ^ <*y*> by A3, FINSEQ_1:46;
A6: len p = (len q) + (len <*y*>) by A5, FINSEQ_1:22;
A7: len <*y*> = 1 by FINSEQ_1:39;

per cases ( q = {} or q <> {} ) ;

suppose A8: q = {} ; :: thesis: ex x being object ex q being FinSequence st
( q = <*b₃*> ^ b₄ & len q = (len b₄) + 1 )

then p = <*y*> by A5, FINSEQ_1:34
.= <*y*> ^ {} by FINSEQ_1:34 ;
hence ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) by A7, A6, A8; :: thesis: verum

end;

suppose q <> {} ; :: thesis: ex x being object ex q being FinSequence st
( q = <*b₃*> ^ b₄ & len q = (len b₄) + 1 )

then consider x being object , r being FinSequence such that
A9: q = <*x*> ^ r and
A10: len q = (len r) + 1 by A2, A4, A7, A6;
A11: len (r ^ <*y*>) = (len r) + 1 by A7, FINSEQ_1:22;
p = <*x*> ^ (r ^ <*y*>) by A5, A9, FINSEQ_1:32;
hence ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) by A7, A6, A10, A11; :: thesis: verum

end;

end;

end;

then A12: for i being Nat st S₁[i] holds
S₁[i + 1] ;
A13: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A13, A12);
hence ex x being object ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) by A1; :: thesis: verum