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

now

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 )
assume A1: i in dom C ; :: thesis: ex u being Element of L ex a being Element of P st C /. i = u * a
then A2: ( dom C c= dom A & C . i = A . i ) by FUNCT_1:70, RELAT_1:89;
then A3: C /. i = A . i by A1, PARTFUN1:def 8
.= A /. i by A1, A2, PARTFUN1:def 8 ;
consider u being Element of L, a being Element of P such that
A4: A /. i = u * a by A1, A2, IDEAL_1:def 10;
thus ex u being Element of L ex a being Element of P st C /. i = u * a by A3, A4; :: thesis: verum

end;

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