let p be FinSequence; :: thesis: ( p <> {} implies ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) )
assume A1: p <> {} ; :: thesis: ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 )
defpred S₁[ Element of NAT ] means for p being FinSequence st p <> {} & len p = $1 holds
ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 );
A2: S₁[ 0 ] ;
A3: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

now

let i be Element of NAT ; :: thesis: ( ( for p being FinSequence st p <> {} & len p = i holds
ex x being set 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 set ex q being FinSequence st
( q = <*b₄*> ^ b₅ & len q = (len b₅) + 1 ) )
assume A4: for p being FinSequence st p <> {} & len p = i holds
ex x being set 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 set 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 set ex q being FinSequence st
( q = <*b₃*> ^ b₄ & len q = (len b₄) + 1 ) )
assume A5: ( p <> {} & len p = i + 1 ) ; :: thesis: ex x being set ex q being FinSequence st
( q = <*b₃*> ^ b₄ & len q = (len b₄) + 1 )
then consider q being FinSequence, y being set such that
A6: p = q ^ <*y*> by FINSEQ_1:63;
A7: ( len <*y*> = 1 & len p = (len q) + (len <*y*>) ) by A6, FINSEQ_1:35, FINSEQ_1:56;

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

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

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

end;

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

then consider x being set , r being FinSequence such that
A9: ( q = <*x*> ^ r & len q = (len r) + 1 ) by A4, A5, A7;
( p = <*x*> ^ (r ^ <*y*>) & len (r ^ <*y*>) = (len r) + 1 & len <*x*> = 1 ) by A6, A7, A9, FINSEQ_1:35, FINSEQ_1:45, FINSEQ_1:56;
hence ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) by A7, A9; :: thesis: verum

end;

end;

end;

hence for i being Element of NAT st S₁[i] holds
S₁[i + 1] ; :: thesis: verum

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A2, A3);
hence ex x being set ex q being FinSequence st
( p = <*x*> ^ q & len p = (len q) + 1 ) by A1; :: thesis: verum