let R be non empty associative commutative multLoopStr ; :: thesis: for A being non empty Subset of R
for f being LinearCombination of A holds
( f is LeftLinearCombination of A & f is RightLinearCombination of A )
let A be non empty Subset of R; :: thesis: for f being LinearCombination of A holds
( f is LeftLinearCombination of A & f is RightLinearCombination of A )
let f be LinearCombination of A; :: thesis: ( f is LeftLinearCombination of A & f is RightLinearCombination of A )
hereby :: according to IDEAL_1:def 9 :: thesis: f is RightLinearCombination of A
let i be set ; :: thesis: ( i in dom f implies ex r being Element of R ex a being Element of A st f /. i = r * a )
assume i in dom f ; :: thesis: ex r being Element of R ex a being Element of A st f /. i = r * a
then consider r, s being Element of R, a being Element of A such that
A1: f /. i = (r * a) * s by Def8;
f /. i = (r * s) * a by A1, GROUP_1:def 3;
hence ex r being Element of R ex a being Element of A st f /. i = r * a ; :: thesis: verum
end;
let i be set ; :: according to IDEAL_1:def 10 :: thesis: ( i in dom f implies ex u being Element of R ex a being Element of A st f /. i = a * u )
assume i in dom f ; :: thesis: ex u being Element of R ex a being Element of A st f /. i = a * u
then consider r, s being Element of R, a being Element of A such that
A2: f /. i = (r * a) * s by Def8;
f /. i = a * (r * s) by A2, GROUP_1:def 3;
hence ex r being Element of R ex a being Element of A st f /. i = a * r ; :: thesis: verum