let R be non empty left_unital multLoopStr ; :: thesis: for A being non empty Subset of R
for f being RightLinearCombination of A holds f is LinearCombination of A
let A be non empty Subset of R; :: thesis: for f being RightLinearCombination of A holds f is LinearCombination of A
let f be RightLinearCombination of A; :: thesis: f is LinearCombination of A
let i be set ; :: according to IDEAL_1:def 8 :: thesis: ( i in dom f implies ex u, v being Element of R ex a being Element of A st f /. i = (u * a) * v )
assume i in dom f ; :: thesis: ex u, v being Element of R ex a being Element of A st f /. i = (u * a) * v
then consider r being Element of R, a being Element of A such that
A1: f /. i = a * r by Def10;
f /. i = ((1. R) * a) * r by A1;
hence ex u, v being Element of R ex a being Element of A st f /. i = (u * a) * v ; :: thesis: verum