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 :: thesis: ( ( j <= len A & A /^ j is LeftLinearCombination of P ) or ( not j <= len A & A /^ j is LeftLinearCombination of P ) )

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

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 )
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 ;
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: verum

end;

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

end;

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

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: verum

end;

end;

end;

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