let p be FinSequence; :: thesis: ( p <> {} implies ex q being FinSequence ex x being set st
( p = q ^ <*x*> & len p = (len q) + 1 ) )
assume A: p <> {} ; :: thesis: ex q being FinSequence ex x being set st
( p = q ^ <*x*> & len p = (len q) + 1 )
consider q being FinSequence, x being set such that
B: p = q ^ <*x*> by A, FINSEQ_1:63;
take q ; :: thesis: ex x being set 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 B, FINSEQ_1:35
.= (len q) + 1 by FINSEQ_1:57 ;
hence ( p = q ^ <*x*> & len p = (len q) + 1 ) by B; :: thesis: verum