let R be non empty right_unital multLoopStr ; :: thesis: for A being non empty Subset of R
for f being LeftLinearCombination of A holds f is LinearCombination of A
let A be non empty Subset of R; :: thesis: for f being LeftLinearCombination of A holds f is LinearCombination of A
let f be LeftLinearCombination 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 = r * a by Def9;
f /. i = (r * a) * (1. 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