set c = NonNegElements v;
set a = the addF of K | [:(NonNegElements v),(NonNegElements v):];
set m = the multF of K | [:(NonNegElements v),(NonNegElements v):];
set j = 1. K;
set z = 0. K;
A2: NonNegElements v c= the carrier of K by Th48;

let x be set ; :: thesis:
assume A3: x in [:(NonNegElements v),(NonNegElements v):] ; :: thesis:
set q = the addF of K . x;
consider x1, x2 being object such that
A4: x1 in NonNegElements v and
A5: x2 in NonNegElements v and
A6: x = [x1,x2] by A3, ZFMISC_1:def 2;
consider y1 being Element of K such that
A7: y1 = x1 and
A8: 0 <= v . y1 by A4;
consider y2 being Element of K such that
A9: y2 = x2 and
A10: 0 <= v . y2 by A5;
A11: min ((v . y1),(v . y2)) <= v . (y1 + y2) by A1, Th27;
0 <= min ((v . y1),(v . y2)) by A8, A10, XXREAL_0:20;
hence the addF of K . x in NonNegElements v by A6, A7, A11, A9; :: thesis:

end;

then reconsider ca = NonNegElements v as Preserv of the addF of K by A2, REALSET1:def 1;
the addF of K || ca is BinOp of (NonNegElements v) ;
then reconsider a = the addF of K | [:(NonNegElements v),(NonNegElements v):] as BinOp of (NonNegElements v) ;

now :: thesis:

let x be set ; :: thesis:
assume A12: x in [:(NonNegElements v),(NonNegElements v):] ; :: thesis:
set q = the multF of K . x;
consider x1, x2 being object such that
A13: x1 in NonNegElements v and
A14: x2 in NonNegElements v and
A15: x = [x1,x2] by A12, ZFMISC_1:def 2;
consider y1 being Element of K such that
A16: y1 = x1 and
A17: 0 <= v . y1 by A13;
consider y2 being Element of K such that
A18: y2 = x2 and
A19: 0 <= v . y2 by A14;
0 + 0 <= (v . y1) + (v . y2) by A17, A19;
then 0 <= v . (y1 * y2) by A1, Def8;
hence the multF of K . x in NonNegElements v by A15, A16, A18; :: thesis:

end;

then reconsider cm = NonNegElements v as Preserv of the multF of K by A2, REALSET1:def 1;
the multF of K || cm is BinOp of (NonNegElements v) ;
then reconsider m = the multF of K | [:(NonNegElements v),(NonNegElements v):] as BinOp of (NonNegElements v) ;
A20: v . (0. K) = +infty by A1, Def8;
reconsider j = 1. K, z = 0. K as Element of NonNegElements v by A1, Th49, Th50;
set R = doubleLoopStr(# (NonNegElements v),a,m,j,z #);
z in NonNegElements v by A20;
then reconsider R = doubleLoopStr(# (NonNegElements v),a,m,j,z #) as non empty doubleLoopStr ;

A21: now :: thesis:

let x, y be Element of R; :: thesis:
let x1, y1 be Element of K; :: thesis:
assume A22: ( x = x1 & y = y1 ) ; :: thesis:
[x,y] in [:(NonNegElements v),(NonNegElements v):] ;
hence x + y = x1 + y1 by A22, FUNCT_1:49; :: thesis:

end;

A23: now :: thesis:

let x, y be Element of R; :: thesis:
let x1, y1 be Element of K; :: thesis:
assume A24: ( x = x1 & y = y1 ) ; :: thesis:
[x,y] in [:(NonNegElements v),(NonNegElements v):] ;
hence x * y = x1 * y1 by A24, FUNCT_1:49; :: thesis:

end;

A25: now :: thesis:

let x, e be Element of R; :: thesis:
assume A26: e = j ; :: thesis:
reconsider x1 = x, e1 = e as Element of K by A2;
thus x * e = x1 * e1 by A23
.= x by A26 ; :: thesis:
thus e * x = e1 * x1 by A23
.= x by A26 ; :: thesis:

end;

R is well-unital by A25;
then reconsider R = R as non empty well-unital doubleLoopStr ;
( R is Abelian & R is add-associative & R is right_zeroed & R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )

proof

hereby :: according to RLVECT_1:def 2 :: thesis:

let x, y be Element of R; :: thesis:
reconsider x1 = x, y1 = y as Element of K by A2;
thus x + y = x1 + y1 by A21
.= y + x by A21 ; :: thesis:

end;

hereby :: according to RLVECT_1:def 3 :: thesis:

let x, y, z be Element of R; :: thesis:
reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;
A27: y + z = y1 + z1 by A21;
x + y = x1 + y1 by A21;
hence (x + y) + z = (x1 + y1) + z1 by A21
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= x + (y + z) by A27, A21 ;
:: thesis:

end;

hereby :: according to RLVECT_1:def 4 :: thesis:

let x be Element of R; :: thesis:
reconsider x1 = x as Element of K by A2;
thus x + (0. R) = x1 + (0. K) by A21
.= x by RLVECT_1:def 4 ; :: thesis:

end;

thus R is right_complementable :: thesis:

proof

let x be Element of R; :: according to ALGSTR_0:def 16 :: thesis:
reconsider x1 = x as Element of K by A2;
consider w1 being Element of K such that
A28: x1 + w1 = 0. K by ALGSTR_0:def 11;
A29: v . (x1 + w1) = +infty by A1, A28, Def8;

per cases ;

suppose v . w1 < v . x1 ; :: thesis:

then v . w1 = v . (w1 + x1) by A1, Th28;
then reconsider w = w1 as Element of R by A29, Th47;
take w ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + w = 0. R by A28, A21; :: thesis:

end;

suppose A30: v . x1 <= v . w1 ; :: thesis:

0 <= v . x1 by Th47;
then reconsider w = w1 as Element of R by A30, Th47;
take w ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + w = 0. R by A28, A21; :: thesis:

end;

hereby :: according to GROUP_1:def 12 :: thesis:

let x, y be Element of R; :: thesis:
reconsider x1 = x, y1 = y as Element of K by A2;
thus x * y = x1 * y1 by A23
.= y * x by A23 ; :: thesis:

end;

hereby :: according to GROUP_1:def 3 :: thesis:

let x, y, z be Element of R; :: thesis:
reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;
A31: y * z = y1 * z1 by A23;
x * y = x1 * y1 by A23;
hence (x * y) * z = (x1 * y1) * z1 by A23
.= x1 * (y1 * z1) by GROUP_1:def 3
.= x * (y * z) by A31, A23 ;
:: thesis:

end;

hereby :: according to VECTSP_1:def 7 :: thesis:

let x, y, z be Element of R; :: thesis:
reconsider x1 = x, y1 = y, z1 = z as Element of K by A2;
A32: y + z = y1 + z1 by A21;
A33: x * y = x1 * y1 by A23;
A34: x * z = x1 * z1 by A23;
A35: y * x = y1 * x1 by A23;
A36: z * x = z1 * x1 by A23;
thus x * (y + z) = x1 * (y1 + z1) by A32, A23
.= (x1 * y1) + (x1 * z1) by VECTSP_1:def 2
.= (x * y) + (x * z) by A21, A33, A34 ; :: thesis:
thus (y + z) * x = (y1 + z1) * x1 by A32, A23
.= (y1 * x1) + (z1 * x1) by VECTSP_1:def 2
.= (y * x) + (z * x) by A21, A35, A36 ; :: thesis:

end;

thus 0. R <> 1. R ; :: according to STRUCT_0:def 8 :: thesis:

end;

hence ex b₁ being non degenerated strict commutative Ring st
( the carrier of b₁ = NonNegElements v & the addF of b₁ = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b₁ = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b₁ = 0. K & the OneF of b₁ = 1. K ) ; :: thesis: