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

now :: thesis: for i being set st i in dom p holds
ex v being Element of R ex a being Element of A st p /. i = a * v

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 A3: i in dom p ; :: thesis: ex v being Element of R ex a being Element of A st p /. i = a * v
take v = the Element of R; :: thesis: ex a being Element of A st p /. i = a * v
take a = the Element of A; :: thesis: p /. i = a * v
i in {1} by A3, FINSEQ_1:2, FINSEQ_1:38;
then i = 1 by TARSKI:def 1;
hence p /. i = a * v by FINSEQ_4:16; :: thesis: verum

end;

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