let R be non empty associative multLoopStr ; :: thesis: for A being non empty Subset of R
for a being Element of R
for F being LinearCombination of A holds F * a is LinearCombination of A
let A be non empty Subset of R; :: thesis: for a being Element of R
for F being LinearCombination of A holds F * a is LinearCombination of A
let a be Element of R; :: thesis: for F being LinearCombination of A holds F * a is LinearCombination of A
let F be LinearCombination of A; :: thesis: F * a is LinearCombination of A
let i be set ; :: according to IDEAL_1:def 8 :: thesis: ( i in dom (F * a) implies ex u, v being Element of R ex a being Element of A st (F * a) /. i = (u * a) * v )
assume i in dom (F * a) ; :: thesis: ex u, v being Element of R ex a being Element of A st (F * a) /. i = (u * a) * v
then A1: i in dom F by POLYNOM1:def 2;
then consider u, v being Element of R, b being Element of A such that
A2: F /. i = (u * b) * v by Def9;
take u ; :: thesis: ex v being Element of R ex a being Element of A st (F * a) /. i = (u * a) * v
take x = v * a; :: thesis: ex a being Element of A st (F * a) /. i = (u * a) * x
take b ; :: thesis: (F * a) /. i = (u * b) * x
thus (F * a) /. i = (F /. i) * a by A1, POLYNOM1:def 2
.= (u * (b * v)) * a by A2, GROUP_1:def 3
.= u * ((b * v) * a) by GROUP_1:def 3
.= u * (b * (v * a)) by GROUP_1:def 3
.= (u * b) * x by GROUP_1:def 3 ; :: thesis: verum