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 ;

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 ) )end;

hence
A /^ j is LeftLinearCombination of P
; :: thesis: verumper cases
( j <= len A or not j <= len A )
;

end;

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;

end;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

hence
A /^ j is LeftLinearCombination of P
by IDEAL_1:def 9; :: thesis: verumex 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;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

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