let p be FinSequence; :: thesis: ( p <> {} implies ex q being FinSequence ex x being object st
( p = q ^ <*x*> & len p = (len q) + 1 ) )
assume p <> {} ; :: thesis: ex q being FinSequence ex x being object st
( p = q ^ <*x*> & len p = (len q) + 1 )
then consider q being FinSequence, x being object such that
A1: p = q ^ <*x*> by FINSEQ_1:46;
take q ; :: thesis: ex x being object st
( p = q ^ <*x*> & len p = (len q) + 1 )
take x ; :: thesis: ( p = q ^ <*x*> & len p = (len q) + 1 )
len p = (len q) + (len <*x*>) by A1, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:40 ;
hence ( p = q ^ <*x*> & len p = (len q) + 1 ) by A1; :: thesis: verum