let p be complex-valued FinSequence; :: thesis: ( len p <> 0 implies ex q being complex-valued FinSequence ex d being Complex st p = q ^ <*d*> )
assume len p <> 0 ; :: thesis: ex q being complex-valued FinSequence ex d being Complex st p = q ^ <*d*>
then consider q being FinSequence, d being object such that
A1: p = q ^ <*d*> by CARD_1:27, FINSEQ_1:46;
rng p c= COMPLEX by VALUED_0:def 1;
then A2: p is FinSequence of COMPLEX by FINSEQ_1:def 4;
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 A1, FINSEQ_1:def 7, FINSEQ_2:15;
hence q . i in COMPLEX by A2, FINSEQ_2:11; :: thesis: verum
end;
then A3: q is FinSequence of COMPLEX by FINSEQ_2:12;
len p = (len q) + 1 by A1, FINSEQ_2:16;
then p . (len p) = d by A1, FINSEQ_1:42;
hence ex q being complex-valued FinSequence ex d being Complex st p = q ^ <*d*> by A1, A3; :: thesis: verum