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 ;
then k <= (len A) - j by ;
then A4: k + j <= ((len A) + (- j)) + j by XREAL_1:6;
A5: k <= k + j by NAT_1:11;
1 <= k by ;
then 1 <= k + j by ;
then j + k in Seg (len A) by ;
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 ; :: 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