environ
vocabularies HIDDEN, VECTSP_1, REALSET2, FUNCT_1, MESFUNC1, SUBSET_1, STRUCT_0, RELAT_1, ARYTM_1, ARYTM_3, SUPINF_2, ALGSTR_0, BINOP_1, ZFMISC_1, REALSET3;
notations HIDDEN, TARSKI, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, REALSET2;
definitions ;
theorems FUNCT_2, ZFMISC_1, REALSET2, XBOOLE_0, RLVECT_1, VECTSP_1, STRUCT_0;
schemes BINOP_1;
registrations RELSET_1, STRUCT_0, REALSET2;
constructors HIDDEN, BINOP_1, REALSET2, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1, REALSET2, ALGSTR_0, STRUCT_0;
expansions ;
theorem Th4:
for
F being
Field for
a,
b,
c,
d being
Element of
F holds
(
a - b = c - d iff
a + d = b + c )
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;
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;
definition
let F be
Field;
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;