let L be non empty multLoopStr ; :: thesis:
let P be non empty Subset of L; :: thesis:
let A be LeftLinearCombination of P; :: thesis:
let j be Element of NAT ; :: thesis:
set C = A /^ j;
reconsider C = A /^ j as FinSequence of the carrier of L ;

now :: thesis:

per cases ;

case A1: j <= len A ; :: thesis:

then reconsider m = (len A) - j as Element of NAT by INT_1:5;

now :: thesis:

let i be set ; :: thesis:
assume A2: i in dom C ; :: thesis:
then reconsider k = i as Element of NAT ;
A3: dom C = Seg (len C) by FINSEQ_1:def 3
.= Seg m by A1, RFINSEQ:def 1 ;
then k <= (len A) - j by A2, FINSEQ_1:1;
then A4: k + j <= ((len A) + (- j)) + j by XREAL_1:6;
A5: k <= k + j by NAT_1:11;
1 <= k by A2, A3, FINSEQ_1:1;
then 1 <= k + j by A5, XXREAL_0:2;
then j + k in Seg (len A) by A4, FINSEQ_1:1;
then j + k in dom A by FINSEQ_1:def 3;
then ex u being Element of L ex a being Element of P st A /. (j + k) = u * a by IDEAL_1:def 9;
hence ex u being Element of L ex a being Element of P st C /. i = u * a by A2, FINSEQ_5:27; :: thesis:

end;

hence A /^ j is LeftLinearCombination of P by IDEAL_1:def 9; :: thesis:

end;

case not j <= len A ; :: thesis:

then C = <*> the carrier of L by RFINSEQ:def 1;
then 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 ;
hence A /^ j is LeftLinearCombination of P by IDEAL_1:def 9; :: thesis:

end;

end;

end;

hence A /^ j is LeftLinearCombination of P ; :: thesis: