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 /^ j;
reconsider C = A /^ j as FinSequence of the carrier of L ;

now

per cases ( j <= len A or not j <= len A ) ;

case A1: j <= len A ; :: thesis: A /^ j is LeftLinearCombination of P

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

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 A2: i in dom C ; :: thesis: ex u being Element of L ex a being Element of P st C /. i = u * a
then reconsider k = i as Element of NAT ;
dom C = Seg (len C) by FINSEQ_1:def 3
.= Seg m by A1, RFINSEQ:def 2 ;
then A3: ( 1 <= k & k <= (len A) - j ) by A2, FINSEQ_1:3;
then A4: k + j <= ((len A) + (- j)) + j by XREAL_1:8;
k <= k + j by NAT_1:11;
then 1 <= k + j by A3, XXREAL_0:2;
then j + k in Seg (len A) by A4, FINSEQ_1:3;
then j + k in dom A by FINSEQ_1:def 3;
then consider u being Element of L, a being Element of P such that
A5: A /. (j + k) = u * a by IDEAL_1:def 10;
thus ex u being Element of L ex a being Element of P st C /. i = u * a by A2, A5, FINSEQ_5:30; :: thesis: verum

end;

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

end;

case not j <= len A ; :: thesis: A /^ j is LeftLinearCombination of P

then C = <*> the carrier of L by RFINSEQ:def 2;
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 10; :: thesis: verum

end;

end;

end;

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