:: Several Properties of Fields. Field Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 TARSKI, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, BINOP_1, STRUCT_0,
ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, REALSET2;
constructors BINOP_1, REALSET2, RELSET_1;
registrations RELSET_1, STRUCT_0, REALSET2;
requirements SUBSET, BOOLE;
equalities BINOP_1, REALSET2, ALGSTR_0, STRUCT_0;
theorems FUNCT_2, ZFMISC_1, REALSET2, XBOOLE_0, RLVECT_1, VECTSP_1, STRUCT_0;
schemes BINOP_1;
begin
:: Properties of fields
theorem Th1:
for F being Field holds revf(F).1.F = 1.F
proof
let F be Field;
A1: 1.F is Element of NonZero F by STRUCT_0:2;
then 1.F*1.F = 1.F by REALSET2:6;
hence thesis by A1,REALSET2:22;
end;
theorem Th2:
for F being Field holds for a,b being Element of NonZero F holds
revf(F).(omf(F).(a,revf(F).b)) = omf(F).(b,revf(F).a)
proof
let F be Field;
let a,b be Element of NonZero F;
reconsider revfa = revf(F).a, revfb = revf(F).b as Element of NonZero F;
A1: omf(F).(a,revf(F).b) is Element of NonZero F by REALSET2:24;
A2: omf(F).(b,revf(F).a) is Element of NonZero F by REALSET2:24;
revfb*(b*revfa) = revfa*(b*revfb) by REALSET2:4
.= revfa*(omf F).(b,revfb)
.= revfa*1.F by REALSET2:def 6
.= revf(F).a by REALSET2:6;
then a*revfb*(b*revfa) = a*revfa by A2,REALSET2:4
.= (omf F).(a,revfa)
.= 1.F by REALSET2:def 6;
hence thesis by A1,A2,REALSET2:22;
end;
theorem Th3:
for F being Field, a,b being Element of NonZero F holds revf(F).(
omf(F).(a,b)) = omf(F).(revf(F).a,revf(F).b)
proof
let F be Field;
let a,b be Element of NonZero F;
reconsider revfa = revf(F).a, revfb = revf(F).b as Element of NonZero F;
thus revf(F).(omf(F).(a,b)) = revf(F).(omf(F).(a,revf(F).(revf(F).b))) by
REALSET2:23
.= revfb*revfa by Th2
.= revfa*revfb
.= omf(F).(revf(F).a,revf(F).b);
end;
theorem Th4:
for F being Field holds for a,b,c,d being Element
of F holds a-b = c-d iff a+d = b+c
proof
let F be Field;
let a,b,c,d be Element of F;
hereby
assume a-b = c-d;
then c-d+b = a+-b+b .= a+(b-b) by RLVECT_1:def 3
.= a+0.F by RLVECT_1:5
.= a by RLVECT_1:4;
hence a+d = c+b+-d+d by RLVECT_1:def 3
.= c+b+(d-d) by RLVECT_1:def 3
.= c+b+0.F by RLVECT_1:5
.= b+c by RLVECT_1:4;
end;
assume a+d = b+c;
then b+c-d = a+(d-d) by RLVECT_1:def 3
.= a+0.F by RLVECT_1:5
.= a by RLVECT_1:4;
hence a-b = c-d+b-b by RLVECT_1:def 3
.= c-d+(b-b) by RLVECT_1:def 3
.= c-d+0.F by RLVECT_1:5
.= c-d by RLVECT_1:4;
end;
theorem Th5:
for F being Field holds for a,c being Element of F
holds for b,d being Element of NonZero F holds omf(F).(a,revf(F).b) = omf(F).(c
,revf(F).d) iff omf(F).(a,d) = omf(F).(b,c)
proof
let F be Field;
let a,c be Element of F;
let b,d be Element of NonZero F;
A1: omf(F).(a,revf(F).b) = omf(F).(c,revf(F).d) implies omf(F).(a,d) = omf(F
).(b,c)
proof
reconsider revfb = revf(F).b, revfd = revf(F).d as Element of NonZero F;
reconsider crevfd = c*revfd as Element of F;
assume
A2: omf(F).(a,revf(F).b) = omf(F).(c,revf(F).d);
A3: c = c*1.F by REALSET2:21
.= omf(F).(c,d*revfd) by REALSET2:def 6
.= c*(revfd*d)
.= c*revfd*d by REALSET2:19;
a = a*1.F by REALSET2:21
.= omf(F).(a,b*revfb) by REALSET2:def 6
.= a*(revfb*b)
.= a*revfb*b by REALSET2:19
.= b*crevfd by A2
.= omf(F).(b,omf(F).(c,revf(F).d));
hence omf(F).(a,d) = b*(c*revfd)*d .= b*(c*revfd*d) by REALSET2:19
.= omf(F).(b,c) by A3;
end;
omf(F).(a,d) = omf(F).(b,c) implies omf(F).(a,revf(F).b) = omf(F).(c,
revf(F).d)
proof
reconsider revfd = revf(F).d, revfb = revf(F).b as Element of NonZero F;
reconsider crevfd = omf(F).(c,revfd) as Element of F;
assume
A4: omf(F).(a,d) = omf(F).(b,c);
a = a*1.F by REALSET2:21
.= omf(F).(a,1.F)
.= a*(d*revfd) by REALSET2:def 6
.= a*d*revfd by REALSET2:19
.= b*c*revfd by A4
.= b*(c*revfd) by REALSET2:19
.= crevfd*b;
hence omf(F).(a,revf(F).b) = crevfd*b*revfb
.= crevfd*(b*revfb) by REALSET2:19
.= omf(F).(c,revfd)*1.F by REALSET2:def 6
.= omf(F).(c,revf(F).d) by REALSET2:21;
end;
hence thesis by A1;
end;
theorem
for F being Field holds for a,b being Element of F
holds for c,d being Element of NonZero F holds omf(F).(omf(F).(a,revf(F).c),omf
(F).(b,revf(F).d)) = omf(F).(omf(F).(a,b),revf(F).(omf(F).(c,d)))
proof
let F be Field;
let a,b be Element of F;
let c,d be Element of NonZero F;
reconsider revfc = revf(F).c, revfd = revf(F).d as Element of NonZero F;
omf(F).(c,d) is Element of NonZero F by REALSET2:24;
then reconsider revfcd = revf(F).(c*d) as Element of F by REALSET2:24;
thus omf(F).(omf(F).(a,revf(F).c),omf(F).(b,revf(F).d)) = a*revfc*(b*revfd)
.= a*(revfc*(b*revfd)) by REALSET2:19
.= a*(b*(revfc*revfd)) by REALSET2:19
.= omf(F).(a,omf(F).(b,revf(F).(omf(F).(c,d)))) by Th3
.= a*(b*revfcd)
.= a*b*revfcd by REALSET2:19
.= omf(F).(omf(F).(a,b),revf(F).(omf(F).(c,d)));
end;
theorem
for F being Field holds for a,b being Element of F
holds 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)))
proof
let F be Field;
let a,b be Element of F;
let c,d be Element of NonZero F;
reconsider revfd = revf(F).d as Element of F by XBOOLE_0:def 5;
A1: a = a*1.F by REALSET2:21
.= omf(F).(a,1.F)
.= a*(d*revfd) by REALSET2:def 6
.= a*d*revfd by REALSET2:19;
reconsider revfc = revf(F).c, revfd = revf(F).d as Element of NonZero F;
omf(F).(c,d) is Element of NonZero F by REALSET2:24;
then reconsider revfcd = revf(F).(c*d) as Element of F by REALSET2:24;
b = b*1.F by REALSET2:21
.= omf(F).(b,1.F)
.= b*(c*revfc) by REALSET2:def 6
.= b*c*revfc by REALSET2:19;
then
A2: omf(F).(b,revf(F).d) = b*c*revfc*revfd .= b*c*(revfc*revfd) by REALSET2:19
.= omf(F).(omf(F).(b,c),revf(F).(omf(F).(c,d))) by Th3;
omf(F).(a,revf(F).c) = a*d*revfd*revfc by A1
.= a*d*(revfd*revfc) by REALSET2:19
.= omf(F).(omf(F).(a,d),revfc*revfd)
.= omf(F).(omf(F).(a,d),revf(F).(omf(F).(c,d))) by Th3;
hence (the addF of F).(omf(F).(a,revf(F).c),omf(F).(b,revf(F).d)) = a*d*
revfcd+b*c*revfcd by A2
.= (a*d+b*c)*revfcd by VECTSP_1:def 7
.= omf(F).((the addF of F). (omf(F).(a,d),omf(F).(b,c)),revf(F).(omf(F).
(c,d)));
end;
definition ::subtraction
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
proof
defpred P[Element of F,Element of F,set]
means $3=(the addF of F).($1,(comp F).$2);
A1: for x being Element of F for y being Element of F ex z being Element
of F st P[x,y,z];
ex f being BinOp of the carrier of F st for x being Element
of F for y being Element of F holds P[x,y,f.(x,y)] from
BINOP_1:sch 3(A1);
then consider S being BinOp of the carrier of F such that
A2: for x,y being Element of F holds S.(x,y)=(the addF of F).(x,(comp F).y);
take S;
thus thesis by A2;
end;
uniqueness
proof
let S1,S2 be BinOp of the carrier of F such that
A3: for x,y being Element of F holds S1.(x,y) = (the
addF of F).(x,(comp F).y) and
A4: for x,y being Element of F holds S2.(x,y) = (the addF of F).(x,(comp F).y);
now
let p be object;
assume p in [:the carrier of F,the carrier of F:];
then consider x,y being object such that
A5: x in the carrier of F & y in the carrier of F and
A6: p=[x,y] by ZFMISC_1:def 2;
thus S1.p = S1.(x,y) by A6
.= (the addF of F).(x,(comp F).y) by A3,A5
.= S2.(x,y) by A4,A5
.= S2.p by A6;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem
for F being Field holds for x being Element of F holds osf(F).(x,x) = 0.F
proof
let F be Field;
let x be Element of F;
thus osf(F).(x,x) = (the addF of F).(x,(comp F).x) by Def1
.= x-x by VECTSP_1:def 13
.= 0.F by RLVECT_1:5;
end;
theorem Th9:
for F being Field holds for a,b,c being Element
of F holds omf(F).(a,osf(F).(b,c)) = osf(F).(omf(F).(a,b),omf(F).(a,c))
proof
let F be Field;
let a,b,c be Element of F;
thus omf(F).(a,osf(F).(b,c)) = omf(F).(a,(the addF of F).(b,(comp F).c)) by
Def1
.= a*(b-c) by VECTSP_1:def 13
.= a*b-a*c by REALSET2:11
.= (the addF of F).(omf(F).(a,b),(comp F).(a*c)) by VECTSP_1:def 13
.= osf(F).(omf(F).(a,b),omf(F).(a,c)) by Def1;
end;
theorem
for F being Field holds for a,b,c being Element of F
holds omf(F).(osf(F).(a,b),c) = osf(F).(omf(F).(a,c),omf(F).(b,c))
proof
let F be Field;
let a,b,c be Element of F;
thus omf(F).(osf(F).(a,b),c) =osf(F).(a,b)*c .= c*osf(F).(a,b)
.= omf(F).(c,osf(F).(a,b))
.= osf(F).(c*a,c*b) by Th9
.= osf(F).(a*c,b*c)
.= osf(F).(omf(F).(a,c),omf(F).(b,c));
end;
theorem
for F being Field holds for a,b being Element of F
holds osf(F).(a,b) = (comp F).(osf(F).(b,a))
proof
let F be Field;
let a,b be Element of F;
osf(F).(a,b) = (the addF of F).(a,(comp F).b) by Def1
.= a+-b by VECTSP_1:def 13
.= -(b-a) by RLVECT_1:33
.= (comp F).(b+-a) by VECTSP_1:def 13
.= (comp F).((the addF of F).(b,(comp F).a)) by VECTSP_1:def 13;
hence thesis by Def1;
end;
theorem
for F being Field holds for a,b being Element of F
holds osf(F).((comp F).a,b) = (comp F).((the addF of F).(a,b))
proof
let F be Field;
let a,b be Element of F;
thus osf(F).((comp F).a,b) = (the addF of F).((comp F).a,(comp F).b) by Def1
.= (the addF of F).(-a,(comp F).b) by VECTSP_1:def 13
.= -a+-b by VECTSP_1:def 13
.= -(a+b) by RLVECT_1:31
.= (comp F).((the addF of F).(a,b)) by VECTSP_1:def 13;
end;
theorem Th13:
for F being Field holds for a,b,c,d being Element
of F holds osf(F).(a,b) = osf(F).(c,d) iff a+d = b+c
proof
let F be Field;
let a,b,c,d be Element of F;
A1: osf(F).(c,d) = (the addF of F).(c,(comp F).d) by Def1
.= c-d by VECTSP_1:def 13;
osf(F).(a,b) = (the addF of F).(a,(comp F).b) by Def1
.= a-b by VECTSP_1:def 13;
hence thesis by A1,Th4;
end;
theorem
for F being Field holds for a being Element of F holds
osf(F).(0.F,a) = (comp F).a
proof
let F be Field;
let a be Element of F;
thus osf(F).(0.F,a) = 0.F+(comp F).a by Def1
.= (comp F).a by REALSET2:2;
end;
theorem Th15:
for F being Field holds for a being Element of F holds osf(F).(a,0.F) = a
proof
let F be Field;
let a be Element of F;
thus osf(F).(a,0.F) = (the addF of F).(a,(comp F).0.F) by Def1
.= (the addF of F).(a,-0.F) by VECTSP_1:def 13
.= a+0.F by RLVECT_1:12
.= a by REALSET2:2;
end;
theorem
for F being Field holds for a,b,c being Element of F
holds a+b = c iff osf(F).(c,a) = b
proof
let F be Field;
let a,b,c be Element of F;
set d=0.F;
c+d = c & osf(F).(b,d) = b by Th15,REALSET2:2;
hence thesis by Th13;
end;
theorem
for F being Field holds for a,b,c being Element of F
holds a+b = c iff osf(F).(c,b) = a
proof
let F be Field;
let a,b,c be Element of F;
set d=0.F;
c+d = c & osf(F).(a,d) = a by Th15,REALSET2:2;
hence thesis by Th13;
end;
theorem
for F being Field holds for a,b,c being Element of F
holds osf(F).(a,osf(F).(b,c)) = (the addF of F).(osf(F).(a,b),c)
proof
let F be Field;
let a,b,c be Element of F;
thus osf(F).(a,osf(F).(b,c)) = osf(F).(a,(the addF of F).(b,(comp F).c)) by
Def1
.= a+(comp F).(b+(comp F).c) by Def1
.= a+(comp F).(b+-c) by VECTSP_1:def 13
.= a+-(b+-c) by VECTSP_1:def 13
.= a+(-b+--c) by RLVECT_1:31
.= a+((comp F).b+--c) by VECTSP_1:def 13
.= a+((comp F).b+(comp F).(-c)) by VECTSP_1:def 13
.= a+((comp F).b+(comp F).((comp F).c)) by VECTSP_1:def 13
.= a+((comp F).b+c) by REALSET2:9
.= a+((comp F).b)+c by RLVECT_1:def 3
.= (the addF of F).(osf(F).(a,b),c) by Def1;
end;
theorem
for F being Field holds for a,b,c being Element of F
holds osf(F).(a,(the addF of F).(b,c)) = osf(F).(osf(F).(a,b),c)
proof
let F be Field;
let a,b,c be Element of F;
thus osf(F).(a,(the addF of F).(b,c)) = (the addF of F).(a,(comp F).((the
addF of F).(b,c))) by Def1
.= a-(b+c) by VECTSP_1:def 13
.= a-b-c by RLVECT_1:27
.= (the addF of F).((the addF of F).(a,-b),(comp F).c) by VECTSP_1:def 13
.= (the addF of F).((the addF of F).(a,(comp F).b),(comp F).c) by
VECTSP_1:def 13
.= (the addF of F).(osf(F).(a,b),(comp F).c) by Def1
.= osf(F).(osf(F).(a,b),c) by Def1;
end;
definition ::division.
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, y being Element of
NonZero F holds it.(x,y) = omf(F).(x,revf(F).y);
existence
proof
defpred P[Element of F, Element of NonZero F,set] means $3=
omf(F).($1,revf(F).$2);
now
let x be Element of F, y be Element of NonZero F;
revf(F).y is Element of F by XBOOLE_0:def 5;
then reconsider
z = omf(F).(x,revf(F).y) as Element of F by REALSET2:10;
take z;
thus z = omf(F).(x,revf(F).y);
end;
then
A1: for x being Element of F for y being Element of NonZero
F ex z being Element of F st P[x,y,z];
ex f being Function of [:the carrier of F, NonZero F:],the carrier of
F st for x being Element of F, y being Element of NonZero F
holds P[x,y,f.(x,y)] from BINOP_1:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let S1,S2 be Function of [:the carrier of F,NonZero F:],the carrier of F
such that
A2: for x being Element of F, y being Element of
NonZero F holds S1.(x,y) = omf(F).(x,revf(F).y) and
A3: for x being Element of F, y being Element of
NonZero F holds S2.(x,y) = omf(F).(x,revf(F).y);
now
let p be object;
assume p in [:the carrier of F,NonZero F:];
then consider x,y being object such that
A4: x in the carrier of F & y in NonZero F and
A5: p=[x,y] by ZFMISC_1:def 2;
S1.(x,y) = omf(F).(x,revf(F).y) by A2,A4
.= S2.(x,y) by A3,A4;
hence S1.p = S2.p by A5;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th20:
for F being Field holds for x being Element of NonZero F holds
ovf(F).(x,x) = 1.F
proof
let F be Field;
let x be Element of NonZero F;
thus ovf(F).(x,x) = omf(F).(x,revf(F).x) by Def2
.=1.F by REALSET2:def 6;
end;
theorem Th21:
for F being Field holds for a,b being Element of
F holds for c being Element of NonZero F holds omf(F).(a,ovf(F).(b,c)) = ovf(F)
.(omf(F).(a,b),c)
proof
let F be Field;
let a,b be Element of F;
let c be Element of NonZero F;
reconsider revfc = revf(F).c as Element of F by XBOOLE_0:def 5;
thus omf(F).(a,ovf(F).(b,c)) = a*(b*revfc) by Def2
.= a*b*revfc by REALSET2:19
.= ovf(F).(omf(F).(a,b),c) by Def2;
end;
theorem
for F being Field holds for a being Element of NonZero F holds omf(F).
(a,ovf(F).(1.F,a)) = 1.F & omf(F).(ovf(F).(1.F,a),a) = 1.F
proof
let F be Field;
let a be Element of NonZero F;
thus
A1: omf(F).(a,ovf(F).(1.F,a)) = ovf(F).(a*1.F,a) by Th21
.= ovf(F).(a,a) by REALSET2:21
.= 1.F by Th20;
thus omf(F).(ovf(F).(1.F,a),a) = ovf(F).(1.F,a)*a .= a*ovf(F).(1.F,a)
.= 1.F by A1;
end;
theorem
for F being Field holds for a,b being Element of NonZero F holds ovf(F
).(a,b) = revf(F).(ovf(F).(b,a))
proof
let F be Field;
let a,b be Element of NonZero F;
ovf(F).(a,b) = omf(F).(a,revf(F).b) by Def2
.= revf(F).(omf(F).(b,revf(F).a)) by Th2;
hence thesis by Def2;
end;
theorem
for F being Field holds for a,b being Element of NonZero F holds ovf(F
).(revf(F).a,b) = revf(F).(omf(F).(a,b))
proof
let F be Field;
let a,b be Element of NonZero F;
revf(F).a is Element of F by XBOOLE_0:def 5;
hence ovf(F).(revf(F).a,b) = omf(F).(revf(F).a,revf(F).b) by Def2
.= revf(F).(omf(F).(a,b)) by Th3;
end;
theorem Th25:
for F being Field holds for a,c being Element of
F holds for b,d being Element of NonZero F holds ovf(F).(a,b) = ovf(F).(c,d)
iff omf(F).(a,d) = omf(F).(b,c)
proof
let F be Field;
let a,c be Element of F;
let b,d be Element of NonZero F;
ovf(F).(a,b) = omf(F).(a,revf(F).b) & ovf(F).(c,d) = omf(F).(c,revf(F).d
) by Def2;
hence thesis by Th5;
end;
theorem
for F being Field holds for a being Element of NonZero F holds ovf(F).
(1.F,a) = revf(F).a
proof
let F be Field;
let a be Element of NonZero F;
reconsider revfa = revf(F).a as Element of NonZero F;
thus ovf(F).(1.F,a) = omf(F).(1.F,revf(F).a) by Def2
.= 1.F*revfa
.= revf(F).a by REALSET2:6;
end;
theorem Th27:
for F being Field holds for a being Element of F holds ovf(F).(a,1.F) = a
proof
let F be Field;
let a be Element of F;
1.F is Element of NonZero F by STRUCT_0:2;
hence ovf(F).(a,1.F) = omf(F).(a,revf(F).1.F) by Def2
.= a*1.F by Th1
.= a by REALSET2:21;
end;
theorem
for F being Field holds for a being Element of NonZero F holds for b,c
being Element of F holds omf(F).(a,b) = c iff ovf(F).(c,a) = b
proof
let F be Field;
let a be Element of NonZero F;
let b,c be Element of F;
set d=1.F;
A1: omf(F).(c,d) =c*1.F .= c by REALSET2:21;
1.F is Element of NonZero F & ovf(F).(b,d) = b by Th27,STRUCT_0:2;
hence thesis by A1,Th25;
end;
theorem
for F being Field holds for a,c being Element of F
holds for b being Element of NonZero F holds omf(F).(a,b) = c iff ovf(F).(c,b)
= a
proof
let F be Field;
let a,c be Element of F;
let b be Element of NonZero F;
set d=1.F;
A1: omf(F).(c,d) = c*1.F .= c by REALSET2:21;
A2: omf(F).(b,a) = b*a .= a*b
.= omf(F).(a,b);
ovf(F).(a,d) = a & 1.F is Element of NonZero F by Th27,STRUCT_0:2;
hence thesis by A1,A2,Th25;
end;
theorem
for F being Field holds for a being Element of F holds
for b,c being Element of NonZero F holds ovf(F).(a,ovf(F).(b,c)) = omf(F).(ovf(
F).(a,b),c)
proof
let F be Field;
let a be Element of F;
let b,c be Element of NonZero F;
A1: omf(F).(b,revf(F).c) is Element of NonZero F by REALSET2:24;
reconsider revfb = revf(F).b as Element of F by XBOOLE_0:def 5;
thus ovf(F).(a,ovf(F).(b,c)) = ovf(F).(a,omf(F).(b,revf(F).c)) by Def2
.= omf(F).(a,revf(F).(omf(F).(b,revf(F).c))) by A1,Def2
.= omf(F).(a,omf(F).(revf(F).b,revf(F).(revf(F).c))) by Th3
.= a*(revfb*c) by REALSET2:23
.= a*revfb*c by REALSET2:19
.= omf(F).(ovf(F).(a,b),c) by Def2;
end;
theorem
for F being Field holds for a being Element of F holds
for b,c being Element of NonZero F holds ovf(F).(a,omf(F).(b,c)) = ovf(F).(ovf(
F).(a,b),c)
proof
let F be Field;
let a be Element of F;
let b,c be Element of NonZero F;
reconsider revfb = revf(F).b, revfc = revf(F).c as Element of F by
XBOOLE_0:def 5;
omf(F).(b,c) is Element of NonZero F by REALSET2:24;
hence ovf(F).(a,omf(F).(b,c)) = omf(F).(a,revf(F).(omf(F).(b,c))) by Def2
.= a*(revfb*revfc) by Th3
.= a*revfb*revfc by REALSET2:19
.= omf(F).(ovf(F).(a,b),revf(F).c) by Def2
.= ovf(F).(ovf(F).(a,b),c) by Def2;
end;