set c = NonNegElements v;
set a = the addF of K | [:(),():];
set m = the multF of K | [:(),():];
set j = 1. K;
set z = 0. K;
A2: NonNegElements v c= the carrier of K by Th48;
now :: thesis: for x being set st x in [:(),():] holds
the addF of K . x in NonNegElements v
let x be set ; :: thesis: ( x in [:(),():] implies the addF of K . x in NonNegElements v )
assume A3: x in [:(),():] ; :: thesis: the addF of K . x in NonNegElements v
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 ;
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 ;
0 <= min ((v . y1),(v . y2)) by ;
hence the addF of K . x in NonNegElements v by A6, A7, A11, A9; :: thesis: verum
end;
then reconsider ca = NonNegElements v as Preserv of the addF of K by ;
the addF of K || ca is BinOp of () ;
then reconsider a = the addF of K | [:(),():] as BinOp of () ;
now :: thesis: for x being set st x in [:(),():] holds
the multF of K . x in NonNegElements v
let x be set ; :: thesis: ( x in [:(),():] implies the multF of K . x in NonNegElements v )
assume A12: x in [:(),():] ; :: thesis: the multF of K . x in NonNegElements v
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 ;
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 ;
then 0 <= v . (y1 * y2) by ;
hence the multF of K . x in NonNegElements v by ; :: thesis: verum
end;
then reconsider cm = NonNegElements v as Preserv of the multF of K by ;
the multF of K || cm is BinOp of () ;
then reconsider m = the multF of K | [:(),():] as BinOp of () ;
A20: v . (0. K) = +infty by ;
reconsider j = 1. K, z = 0. K as Element of NonNegElements v by ;
set R = doubleLoopStr(# (),a,m,j,z #);
z in NonNegElements v by A20;
then reconsider R = doubleLoopStr(# (),a,m,j,z #) as non empty doubleLoopStr ;
A21: now :: thesis: for x, y being Element of R
for x1, y1 being Element of K st x = x1 & y = y1 holds
x + y = x1 + y1
let x, y be Element of R; :: thesis: for x1, y1 being Element of K st x = x1 & y = y1 holds
x + y = x1 + y1

let x1, y1 be Element of K; :: thesis: ( x = x1 & y = y1 implies x + y = x1 + y1 )
assume A22: ( x = x1 & y = y1 ) ; :: thesis: x + y = x1 + y1
[x,y] in [:(),():] ;
hence x + y = x1 + y1 by ; :: thesis: verum
end;
A23: now :: thesis: for x, y being Element of R
for x1, y1 being Element of K st x = x1 & y = y1 holds
x * y = x1 * y1
let x, y be Element of R; :: thesis: for x1, y1 being Element of K st x = x1 & y = y1 holds
x * y = x1 * y1

let x1, y1 be Element of K; :: thesis: ( x = x1 & y = y1 implies x * y = x1 * y1 )
assume A24: ( x = x1 & y = y1 ) ; :: thesis: x * y = x1 * y1
[x,y] in [:(),():] ;
hence x * y = x1 * y1 by ; :: thesis: verum
end;
A25: now :: thesis: for x, e being Element of R st e = j holds
( x * e = x & e * x = x )
let x, e be Element of R; :: thesis: ( e = j implies ( x * e = x & e * x = x ) )
assume A26: e = j ; :: thesis: ( x * e = x & e * x = x )
reconsider x1 = x, e1 = e as Element of K by A2;
thus x * e = x1 * e1 by A23
.= x by A26 ; :: thesis: e * x = x
thus e * x = e1 * x1 by A23
.= x by A26 ; :: thesis: verum
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: ( 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 )
let x, y be Element of R; :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of K by A2;
thus x + y = x1 + y1 by A21
.= y + x by A21 ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 3 :: thesis: ( R is right_zeroed & R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )
let x, y, z be Element of R; :: thesis: (x + y) + z = x + (y + z)
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 ;
:: thesis: verum
end;
hereby :: according to RLVECT_1:def 4 :: thesis: ( R is right_complementable & R is commutative & R is associative & R is distributive & not R is degenerated )
let x be Element of R; :: thesis: x + (0. R) = x
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: verum
end;
thus R is right_complementable :: thesis: ( R is commutative & R is associative & R is distributive & not R is degenerated )
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 ;
per cases ( v . w1 < v . x1 or v . x1 <= v . w1 ) ;
suppose v . w1 < v . x1 ; :: thesis:
then v . w1 = v . (w1 + x1) by ;
then reconsider w = w1 as Element of R by ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: x + w = 0. R
thus x + w = 0. R by ; :: thesis: verum
end;
suppose A30: v . x1 <= v . w1 ; :: thesis:
0 <= v . x1 by Th47;
then reconsider w = w1 as Element of R by ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: x + w = 0. R
thus x + w = 0. R by ; :: thesis: verum
end;
end;
end;
hereby :: according to GROUP_1:def 12 :: thesis: ( R is associative & R is distributive & not R is degenerated )
let x, y be Element of R; :: thesis: x * y = y * x
reconsider x1 = x, y1 = y as Element of K by A2;
thus x * y = x1 * y1 by A23
.= y * x by A23 ; :: thesis: verum
end;
hereby :: according to GROUP_1:def 3 :: thesis: ( R is distributive & not R is degenerated )
let x, y, z be Element of R; :: thesis: (x * y) * z = x * (y * z)
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 ;
:: thesis: verum
end;
hereby :: according to VECTSP_1:def 7 :: thesis: not R is degenerated
let x, y, z be Element of R; :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
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
.= (x1 * y1) + (x1 * z1) by VECTSP_1:def 2
.= (x * y) + (x * z) by ; :: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (y1 + z1) * x1 by
.= (y1 * x1) + (z1 * x1) by VECTSP_1:def 2
.= (y * x) + (z * x) by ; :: thesis: verum
end;
thus 0. R <> 1. R ; :: according to STRUCT_0:def 8 :: thesis: verum
end;
hence ex b1 being non degenerated strict commutative Ring st
( the carrier of b1 = NonNegElements v & the addF of b1 = the addF of K | [:(),():] & the multF of b1 = the multF of K | [:(),():] & the ZeroF of b1 = 0. K & the OneF of b1 = 1. K ) ; :: thesis: verum