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

now

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

end;

hence ( p is RightLinearCombination of A & not p is empty ) by Def11; :: thesis: verum