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 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;

then C is LeftLinearCombination of P by IDEAL_1:def 9;
hence A | j is LeftLinearCombination of P by FINSEQ_1:def 16; :: thesis: verum