let p be complex-yielding FinSequence; :: thesis: ( len p <> 0 implies ex q being complex-yielding FinSequence ex d being complex number st p = q ^ <*d*> )
assume A1: len p <> 0 ; :: thesis: ex q being complex-yielding FinSequence ex d being complex number st p = q ^ <*d*>
then p <> {} by CARD_1:47;
then consider q being FinSequence, d being set such that
A2: p = q ^ <*d*> by FINSEQ_1:63;
rng p c= COMPLEX by VALUED_0:def 1;
then A3: p is FinSequence of COMPLEX by FINSEQ_1:def 4;
A4: for i being Nat st i in dom q holds
q . i in COMPLEX

proof

let i be Nat; :: thesis: ( i in dom q implies q . i in COMPLEX )
assume i in dom q ; :: thesis: q . i in COMPLEX
then ( p . i = q . i & i in dom p ) by A2, FINSEQ_1:def 7, FINSEQ_2:18;
hence q . i in COMPLEX by A3, FINSEQ_2:13; :: thesis: verum

end;

A5: len p in Seg (len p) by A1, FINSEQ_1:5;
len p = (len q) + 1 by A2, FINSEQ_2:19;
then ( len p in dom p & p . (len p) = d ) by A2, A5, FINSEQ_1:59, FINSEQ_1:def 3;
then ( d is Element of COMPLEX & q is FinSequence of COMPLEX ) by A3, A4, FINSEQ_2:13, FINSEQ_2:14;
hence ex q being complex-yielding FinSequence ex d being complex number st p = q ^ <*d*> by A2; :: thesis: verum