let L be non empty multLoopStr ; :: thesis: for P, Q being non empty Subset of L
for A being LeftLinearCombination of P st P c= Q holds
A is LeftLinearCombination of Q
let P, Q be non empty Subset of L; :: thesis: for A being LeftLinearCombination of P st P c= Q holds
A is LeftLinearCombination of Q
let A be LeftLinearCombination of P; :: thesis: ( P c= Q implies A is LeftLinearCombination of Q )
assume A1: P c= Q ; :: thesis: A is LeftLinearCombination of Q

now :: thesis: for i being set st i in dom A holds
ex u being Element of L ex a being Element of Q st A /. i = u * a

let i be set ; :: thesis: ( i in dom A implies ex u being Element of L ex a being Element of Q st A /. i = u * a )
assume i in dom A ; :: thesis: ex u being Element of L ex a being Element of Q st A /. i = u * a
then consider u being Element of L, a being Element of P such that
A2: A /. i = u * a by IDEAL_1:def 9;
a in P ;
hence ex u being Element of L ex a being Element of Q st A /. i = u * a by A1, A2; :: thesis: verum

end;

hence A is LeftLinearCombination of Q by IDEAL_1:def 9; :: thesis: verum