let L be non empty add-cancelable add-associative right_zeroed associative well-unital distributive left_zeroed doubleLoopStr ; :: thesis:
let F be non empty Subset of L; :: thesis:
set I = { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } ;
A1: { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } c= F -RightIdeal

let x be set ; :: according to TARSKI:def 3 :: thesis:
defpred S₁[ Nat] means for lc being RightLinearCombination of F st len lc <= $1 holds
Sum lc in F -RightIdeal ;
A2: S₁[ 0 ]

let lc be RightLinearCombination of F; :: thesis:
assume len lc <= 0 ; :: thesis:
then len lc = 0 ;
then lc = <*> the carrier of L ;
then A3: Sum lc = 0. L by RLVECT_1:60;
consider y being Element of F;
F c= F -RightIdeal by Def17;
then A4: y in F -RightIdeal by TARSKI:def 3;
y * (0. L) = 0. L by BINOM:2;
hence Sum lc in F -RightIdeal by A3, A4, Def3; :: thesis:

end;

A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
assume A6: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

let lc be RightLinearCombination of F; :: thesis:
assume A7: len lc <= k + 1 ; :: thesis:

per cases by A7, NAT_1:8;

suppose len lc <= k ; :: thesis:

hence Sum lc in F -RightIdeal by A6; :: thesis:

end;

suppose A8: len lc = k + 1 ; :: thesis:

then not lc is empty ;
then consider q being RightLinearCombination of F, r being Element of L such that
A9: ( lc = q ^ <*r*> & <*r*> is RightLinearCombination of F ) by Th34;
k + 1 = (len q) + (len <*r*>) by A8, A9, FINSEQ_1:35
.= (len q) + 1 by FINSEQ_1:56 ;
then A10: Sum q in F -RightIdeal by A6;
dom <*r*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then A11: 1 in dom <*r*> by TARSKI:def 1;
then consider v being Element of L, a being Element of F such that
A12: <*r*> /. 1 = a * v by A9, Def11;
A13: <*r*> /. 1 = <*r*> . 1 by A11, PARTFUN1:def 8;
A14: Sum <*r*> = r by BINOM:3
.= a * v by A12, A13, FINSEQ_1:57 ;
F c= F -RightIdeal by Def17;
then a in F -RightIdeal by TARSKI:def 3;
then A15: Sum <*r*> in F -RightIdeal by A14, Def3;
Sum lc = (Sum q) + (Sum <*r*>) by A9, RLVECT_1:58;
hence Sum lc in F -RightIdeal by A10, A15, Def1; :: thesis:

end;

A16: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A5);
assume x in { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } ; :: thesis:
then consider x' being Element of L such that
A17: ( x' = x & ex lc being RightLinearCombination of F st Sum lc = x' ) ;
consider lc being RightLinearCombination of F such that
A18: Sum lc = x' by A17;
S₁[ len lc] by A16;
hence x in F -RightIdeal by A17, A18; :: thesis:

end;

A19: F c= { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x }

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A20: x in F ; :: thesis:
then reconsider x = x as Element of L ;
set lc = <*x*>;

let i be set ; :: thesis:
assume A21: i in dom <*x*> ; :: thesis:
dom <*x*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then i = 1 by A21, TARSKI:def 1;
then <*x*> . i = x by FINSEQ_1:57
.= x * (1. L) by VECTSP_1:def 13 ;
hence ex v being Element of L ex a being Element of F st <*x*> /. i = a * v by A20, A21, PARTFUN1:def 8; :: thesis:

end;

then reconsider lc = <*x*> as RightLinearCombination of F by Def11;
Sum lc = x by BINOM:3;
hence x in { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } ; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } ; :: thesis:
then consider x' being Element of L such that
A23: ( x' = x & ex lc being RightLinearCombination of F st Sum lc = x' ) ;
thus x in the carrier of L by A23; :: thesis:

end;

reconsider I = { x where x is Element of L : ex lc being RightLinearCombination of F st Sum lc = x } as non empty Subset of L by A19, A22;
reconsider I' = I as non empty Subset of L ;
A25: I' is add-closed

let x, y be Element of L; :: according to IDEAL_1:def 1 :: thesis:
assume A26: ( x in I' & y in I' ) ; :: thesis:
then consider x' being Element of L such that
A27: ( x' = x & ex lc being RightLinearCombination of F st Sum lc = x' ) ;
consider y' being Element of L such that
A28: ( y' = y & ex lc being RightLinearCombination of F st Sum lc = y' ) by A26;
consider lcx being RightLinearCombination of F such that
A29: Sum lcx = x' by A27;
consider lcy being RightLinearCombination of F such that
A30: Sum lcy = y' by A28;
Sum (lcx ^ lcy) = x' + y' by A29, A30, RLVECT_1:58;
hence x + y in I' by A27, A28; :: thesis:

end;

I' is right-ideal

let p, x be Element of L; :: according to IDEAL_1:def 3 :: thesis:
assume x in I' ; :: thesis:
then consider x' being Element of L such that
A31: ( x' = x & ex lc being RightLinearCombination of F st Sum lc = x' ) ;
consider lcx being RightLinearCombination of F such that
A32: Sum lcx = x' by A31;
reconsider lcxp = lcx * p as RightLinearCombination of F by Th29;
x * p = Sum lcxp by A31, A32, BINOM:5;
hence x * p in I' ; :: thesis:

end;

then F -RightIdeal c= I by A19, A25, Def17;
then A33: I = F -RightIdeal by A1, XBOOLE_0:def 10;
let x be set ; :: thesis:

hereby :: thesis:

assume x in F -RightIdeal ; :: thesis:
then consider x' being Element of L such that
A34: ( x' = x & ex lc being RightLinearCombination of F st Sum lc = x' ) by A33;
thus ex f being RightLinearCombination of F st x = Sum f by A34; :: thesis:

end;

assume ex f being RightLinearCombination of F st x = Sum f ; :: thesis:
hence x in F -RightIdeal by A33; :: thesis: