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;
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
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
.= A /. i by ;
hence ex u being Element of L ex a being Element of P st C /. i = u * a by ; :: thesis: verum
end;
then C is LeftLinearCombination of P by IDEAL_1:def 9;
hence A | j is LeftLinearCombination of P by FINSEQ_1:def 15; :: thesis: verum