begin
begin
definition
let I be non
degenerated commutative domRing-like Ring;
existence
ex b1 being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b1 . (u,v) = qadd (u,v)
uniqueness
for b1, b2 being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b1 . (u,v) = qadd (u,v) ) & ( for u, v being Element of Quot. I holds b2 . (u,v) = qadd (u,v) ) holds
b1 = b2
end;
definition
let I be non
degenerated commutative domRing-like Ring;
existence
ex b1 being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b1 . (u,v) = qmult (u,v)
uniqueness
for b1, b2 being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b1 . (u,v) = qmult (u,v) ) & ( for u, v being Element of Quot. I holds b2 . (u,v) = qmult (u,v) ) holds
b1 = b2
end;
begin
Lm2:
for I being non degenerated commutative domRing-like Ring holds
( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable )
Lm3:
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is non empty commutative doubleLoopStr
Lm4:
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is well-unital
begin
begin