let L be non empty multLoopStr ; :: thesis: for P being non empty Subset of L

for A being LeftLinearCombination of P

for i being Element of NAT holds A | i is LeftLinearCombination of P

let P be non empty Subset of L; :: thesis: for A being LeftLinearCombination of P

for i being Element of NAT holds A | i is LeftLinearCombination of P

let A be LeftLinearCombination of P; :: thesis: for i being Element of NAT holds A | i is LeftLinearCombination of P

let j be Element of NAT ; :: thesis: A | j is LeftLinearCombination of P

set C = A | (Seg j);

reconsider C = A | (Seg j) as FinSequence of the carrier of L by FINSEQ_1:18;

hence A | j is LeftLinearCombination of P by FINSEQ_1:def 15; :: thesis: verum

for A being LeftLinearCombination of P

for i being Element of NAT holds A | i is LeftLinearCombination of P

let P be non empty Subset of L; :: thesis: for A being LeftLinearCombination of P

for i being Element of NAT holds A | i is LeftLinearCombination of P

let A be LeftLinearCombination of P; :: thesis: for i being Element of NAT holds A | i is LeftLinearCombination of P

let j be Element of NAT ; :: thesis: A | j is LeftLinearCombination of P

set C = A | (Seg j);

reconsider C = A | (Seg j) as FinSequence of the carrier of L by FINSEQ_1:18;

now :: thesis: for i being set st i in dom C holds

ex u being Element of L ex a being Element of P st C /. i = u * a

then
C is LeftLinearCombination of P
by IDEAL_1:def 9;ex u being Element of L ex a being Element of P st C /. i = u * a

let i be set ; :: thesis: ( i in dom C implies ex u being Element of L ex a being Element of P st C /. i = u * a )

A1: dom C c= dom A by RELAT_1:60;

assume A2: i in dom C ; :: thesis: ex u being Element of L ex a being Element of P st C /. i = u * a

then C . i = A . i by FUNCT_1:47;

then C /. i = A . i by A2, PARTFUN1:def 6

.= A /. i by A2, A1, PARTFUN1:def 6 ;

hence ex u being Element of L ex a being Element of P st C /. i = u * a by A2, A1, IDEAL_1:def 9; :: thesis: verum

end;A1: dom C c= dom A by RELAT_1:60;

assume A2: i in dom C ; :: thesis: ex u being Element of L ex a being Element of P st C /. i = u * a

then C . i = A . i by FUNCT_1:47;

then C /. i = A . i by A2, PARTFUN1:def 6

.= A /. i by A2, A1, PARTFUN1:def 6 ;

hence ex u being Element of L ex a being Element of P st C /. i = u * a by A2, A1, IDEAL_1:def 9; :: thesis: verum

hence A | j is LeftLinearCombination of P by FINSEQ_1:def 15; :: thesis: verum