begin
theorem
canceled;
theorem Th2:
theorem
canceled;
theorem Th4:
theorem
canceled;
theorem Th6:
theorem Th7:
for
F being
Field for
a,
b,
c,
d being
Element of
F holds
(
a - b = c - d iff
a + d = b + c )
theorem Th8:
theorem
canceled;
theorem
theorem
for
F being
Field for
a,
b being
Element of
F for
c,
d being
Element of
NonZero F holds the
addF of
F . ((omf F) . a,((revf F) . c)),
((omf F) . b,((revf F) . d)) = (omf F) . (the addF of F . ((omf F) . a,d),((omf F) . b,c)),
((revf F) . ((omf F) . c,d))
definition
let F be
Field;
func osf F -> BinOp of the
carrier of
F means :
Def1:
for
x,
y being
Element of
F holds
it . x,
y = the
addF of
F . x,
((comp F) . y);
existence
ex b1 being BinOp of the carrier of F st
for x, y being Element of F holds b1 . x,y = the addF of F . x,((comp F) . y)
uniqueness
for b1, b2 being BinOp of the carrier of F st ( for x, y being Element of F holds b1 . x,y = the addF of F . x,((comp F) . y) ) & ( for x, y being Element of F holds b2 . x,y = the addF of F . x,((comp F) . y) ) holds
b1 = b2
end;
:: deftheorem Def1 defines osf REALSET3:def 1 :
theorem
canceled;
theorem
canceled;
theorem
theorem Th15:
theorem
canceled;
theorem
theorem
theorem
theorem Th20:
theorem
theorem Th22:
theorem
theorem
theorem
theorem
definition
let F be
Field;
func ovf F -> Function of
[:the carrier of F,(NonZero F):],the
carrier of
F means :
Def2:
for
x being
Element of
F for
y being
Element of
NonZero F holds
it . x,
y = (omf F) . x,
((revf F) . y);
existence
ex b1 being Function of [:the carrier of F,(NonZero F):],the carrier of F st
for x being Element of F
for y being Element of NonZero F holds b1 . x,y = (omf F) . x,((revf F) . y)
uniqueness
for b1, b2 being Function of [:the carrier of F,(NonZero F):],the carrier of F st ( for x being Element of F
for y being Element of NonZero F holds b1 . x,y = (omf F) . x,((revf F) . y) ) & ( for x being Element of F
for y being Element of NonZero F holds b2 . x,y = (omf F) . x,((revf F) . y) ) holds
b1 = b2
end;
:: deftheorem Def2 defines ovf REALSET3:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem
canceled;
theorem Th31:
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th37:
theorem
theorem Th39:
theorem
theorem
theorem
theorem