consider a being Element of A;
consider u being Element of R;
reconsider p = <*(u * a)*> as FinSequence of the carrier of R ;
take p ; :: thesis: ( p is LeftLinearCombination of A & not p is empty )

now

let i be set ; :: thesis: ( i in dom p implies ex u being Element of R ex a being Element of A st p /. i = u * a )
assume A2: i in dom p ; :: thesis: ex u being Element of R ex a being Element of A st p /. i = u * a
take u = u; :: thesis: ex a being Element of A st p /. i = u * a
take a = a; :: thesis: p /. i = u * a
i in {1} by A2, FINSEQ_1:4, FINSEQ_1:55;
then i = 1 by TARSKI:def 1;
hence p /. i = u * a by FINSEQ_4:25; :: thesis: verum

end;

hence ( p is LeftLinearCombination of A & not p is empty ) by Def10; :: thesis: verum