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

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

hence
A is LeftLinearCombination of Q
by IDEAL_1:def 9; :: thesis: verumex 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;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