:: REALSET2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let IT be LoopStr ;
attr IT is zeroed means :Def1: :: REALSET2:def 1
for a being Element of IT holds
( the add of IT . a,the Zero of IT = a & the add of IT . the Zero of IT,a = a );
attr IT is complementable means :Def2: :: REALSET2:def 2
for a being Element of IT ex b being Element of IT st
( the add of IT . a,b = the Zero of IT & the add of IT . b,a = the Zero of IT );
end;

:: deftheorem Def1 defines zeroed REALSET2:def 1 :
for IT being LoopStr holds
( IT is zeroed iff for a being Element of IT holds
( the add of IT . a,the Zero of IT = a & the add of IT . the Zero of IT,a = a ) );

:: deftheorem Def2 defines complementable REALSET2:def 2 :
for IT being LoopStr holds
( IT is complementable iff for a being Element of IT ex b being Element of IT st
( the add of IT . a,b = the Zero of IT & the add of IT . b,a = the Zero of IT ) );

definition
let L be non empty LoopStr ;
redefine attr L is add-associative means :Def3: :: REALSET2:def 3
for a, b, c being Element of L holds the add of L . (the add of L . a,b),c = the add of L . a,(the add of L . b,c);
compatibility
( L is add-associative iff for a, b, c being Element of L holds the add of L . (the add of L . a,b),c = the add of L . a,(the add of L . b,c) )
proof end;
redefine attr L is Abelian means :Def4: :: REALSET2:def 4
for a, b being Element of L holds the add of L . a,b = the add of L . b,a;
compatibility
( L is Abelian iff for a, b being Element of L holds the add of L . a,b = the add of L . b,a )
proof end;
end;

:: deftheorem Def3 defines add-associative REALSET2:def 3 :
for L being non empty LoopStr holds
( L is add-associative iff for a, b, c being Element of L holds the add of L . (the add of L . a,b),c = the add of L . a,(the add of L . b,c) );

:: deftheorem Def4 defines Abelian REALSET2:def 4 :
for L being non empty LoopStr holds
( L is Abelian iff for a, b being Element of L holds the add of L . a,b = the add of L . b,a );

Lm2: now
consider x being set ;
set B = {x};
A1: x in {x} by TARSKI:def 1;
consider og being BinOp of {x};
A2: og . [x,x] = x
proof
A3: ( dom og = [:{x},{x}:] & rng og c= {x} ) by FUNCT_2:def 1, RELSET_1:12;
[x,x] in [:{x},{x}:] by A1, ZFMISC_1:def 2;
then og . [x,x] in rng og by A3, FUNCT_1:def 5;
hence og . [x,x] = x by A3, TARSKI:def 1; :: thesis: verum
end;
reconsider ng = x as Element of {x} by TARSKI:def 1;
A4: for a, b, c being Element of {x} holds og . (og . a,b),c = og . a,(og . b,c)
proof
let a, b, c be Element of {x}; :: thesis: og . (og . a,b),c = og . a,(og . b,c)
( a = x & b = x & c = x ) by TARSKI:def 1;
hence og . (og . a,b),c = og . a,(og . b,c) by A2; :: thesis: verum
end;
A5: for a being Element of {x} holds
( og . a,ng = a & og . ng,a = a )
proof
let a be Element of {x}; :: thesis: ( og . a,ng = a & og . ng,a = a )
a = x by TARSKI:def 1;
hence ( og . a,ng = a & og . ng,a = a ) by A2; :: thesis: verum
end;
A6: for a being Element of {x} ex b being Element of {x} st
( og . a,b = ng & og . b,a = ng )
proof
let a be Element of {x}; :: thesis: ex b being Element of {x} st
( og . a,b = ng & og . b,a = ng )
take ng ; :: thesis: ( og . a,ng = ng & og . ng,a = ng )
thus ( og . a,ng = ng & og . ng,a = ng ) by TARSKI:def 1; :: thesis: verum
end;
for a, b being Element of {x} holds og . a,b = og . b,a
proof
let a, b be Element of {x}; :: thesis: og . a,b = og . b,a
( a = x & b = x ) by TARSKI:def 1;
hence og . a,b = og . b,a ; :: thesis: verum
end;
hence ex A being non empty set ex og being BinOp of A ex ng being Element of A st
( ( for a, b, c being Element of A holds og . (og . a,b),c = og . a,(og . b,c) ) & ( for a being Element of A holds
( og . a,ng = a & og . ng,a = a ) ) & ( for a being Element of A ex b being Element of A st
( og . a,b = ng & og . b,a = ng ) ) & ( for a, b being Element of A holds og . a,b = og . b,a ) ) by A4, A5, A6; :: thesis: verum
end;

registration
cluster non empty strict Abelian add-associative zeroed complementable LoopStr ;
existence
ex b1 being non empty LoopStr st
( b1 is strict & b1 is Abelian & b1 is add-associative & b1 is zeroed & b1 is complementable )
proof end;
end;

definition
mode Group is non empty Abelian add-associative zeroed complementable LoopStr ;
end;

definition
let IT be 1-sorted ;
attr IT is trivial means :: REALSET2:def 5
the carrier of IT is trivial;
end;

:: deftheorem defines trivial REALSET2:def 5 :
for IT being 1-sorted holds
( IT is trivial iff the carrier of IT is trivial );

Lm3: for S being 1-sorted holds
( S is trivial iff for x, y being Element of S holds x = y )
proof end;

registration
cluster trivial 1-sorted ;
existence
ex b1 being 1-sorted st b1 is trivial
proof end;
end;

Lm4: now
let A be non trivial set ; :: thesis: for od, om being BinOp of A
for nd being Element of A
for nm being Element of A \ {nd}
for nm0 being Element of A st nm0 = nm holds
( not doubleLoopStr(# A,od,om,nm0,nd #) is trivial & doubleLoopStr(# A,od,om,nm0,nd #) is strict )
let od, om be BinOp of A; :: thesis: for nd being Element of A
for nm being Element of A \ {nd}
for nm0 being Element of A st nm0 = nm holds
( not doubleLoopStr(# A,od,om,nm0,nd #) is trivial & doubleLoopStr(# A,od,om,nm0,nd #) is strict )
let nd be Element of A; :: thesis: for nm being Element of A \ {nd}
for nm0 being Element of A st nm0 = nm holds
( not doubleLoopStr(# A,od,om,nm0,nd #) is trivial & doubleLoopStr(# A,od,om,nm0,nd #) is strict )
let nm be Element of A \ {nd}; :: thesis: for nm0 being Element of A st nm0 = nm holds
( not doubleLoopStr(# A,od,om,nm0,nd #) is trivial & doubleLoopStr(# A,od,om,nm0,nd #) is strict )
let nm0 be Element of A; :: thesis: ( nm0 = nm implies ( not doubleLoopStr(# A,od,om,nm0,nd #) is trivial & doubleLoopStr(# A,od,om,nm0,nd #) is strict ) )
assume A1: nm0 = nm ; :: thesis: ( not doubleLoopStr(# A,od,om,nm0,nd #) is trivial & doubleLoopStr(# A,od,om,nm0,nd #) is strict )
set F = doubleLoopStr(# A,od,om,nm0,nd #);
thus not doubleLoopStr(# A,od,om,nm0,nd #) is trivial :: thesis: doubleLoopStr(# A,od,om,nm0,nd #) is strict
proof
now
take nd = nd; :: thesis: ex nm0 being Element of A st nd <> nm0
take nm0 = nm0; :: thesis: nd <> nm0
not nm in {nd} by XBOOLE_0:def 4;
hence nd <> nm0 by A1, TARSKI:def 1; :: thesis: verum
end;
hence not doubleLoopStr(# A,od,om,nm0,nd #) is trivial by Lm3; :: thesis: verum
end;
thus doubleLoopStr(# A,od,om,nm0,nd #) is strict ; :: thesis: verum
end;

registration
cluster strict non trivial doubleLoopStr ;
existence
ex b1 being doubleLoopStr st
( not b1 is trivial & b1 is strict )
proof end;
end;

definition
let A be non trivial set ;
let od, om be BinOp of A;
let nd be Element of A;
let nm be Element of A \ {nd};
func field A,od,om,nd,nm -> strict non trivial doubleLoopStr means :Def6: :: REALSET2:def 6
( A = the carrier of it & od = the add of it & om = the mult of it & nd = the Zero of it & nm = the unity of it );
existence
ex b1 being strict non trivial doubleLoopStr st
( A = the carrier of b1 & od = the add of b1 & om = the mult of b1 & nd = the Zero of b1 & nm = the unity of b1 )
proof end;
uniqueness
for b1, b2 being strict non trivial doubleLoopStr st A = the carrier of b1 & od = the add of b1 & om = the mult of b1 & nd = the Zero of b1 & nm = the unity of b1 & A = the carrier of b2 & od = the add of b2 & om = the mult of b2 & nd = the Zero of b2 & nm = the unity of b2 holds
b1 = b2 ;
end;

:: deftheorem Def6 defines field REALSET2:def 6 :
for A being non trivial set
for od, om being BinOp of A
for nd being Element of A
for nm being Element of A \ {nd}
for b6 being strict non trivial doubleLoopStr holds
( b6 = field A,od,om,nd,nm iff ( A = the carrier of b6 & od = the add of b6 & om = the mult of b6 & nd = the Zero of b6 & nm = the unity of b6 ) );

definition
let IT be 1-sorted ;
redefine attr IT is trivial means :: REALSET2:def 7
for x, y being Element of IT holds x = y;
compatibility
( IT is trivial iff for x, y being Element of IT holds x = y ) by Lm3;
end;

:: deftheorem defines trivial REALSET2:def 7 :
for IT being 1-sorted holds
( IT is trivial iff for x, y being Element of IT holds x = y );

consider x, y being set such that
Lm5: x <> y by VECTSP_1:78;

set Z = {x,y};

Lm6: x in {x,y}
by TARSKI:def 2;

Lm7: y in {x,y}
by TARSKI:def 2;

for s being Element of {x,y} holds {x,y} \ {s} is non empty set
proof end;

then reconsider A = {x,y} as non trivial set by REALSET1:6;

reconsider nd = x as Element of A by TARSKI:def 2;

Lm8: for t being set holds
( t in [:A,A:] iff ( t = [x,x] or t = [x,y] or t = [y,x] or t = [y,y] ) )
proof end;

for t being set holds
( t in [:A,A:] iff t in {[x,x],[x,y],[y,x],[y,y]} )
by Lm8, ENUMSET1:def 2;

Lm9: [:A,A:] = {[x,x],[x,y],[y,x],[y,y]}
by Lm8, ENUMSET1:def 2;

set x1 = [[x,x],x];

set x2 = [[x,y],y];

set x3 = [[y,x],y];

set x4 = [[y,y],x];

set F = {[[x,x],x],[[x,y],y],[[y,x],y],[[y,y],x]};

Lm10: for p being set st p in {[[x,x],x],[[x,y],y],[[y,x],y],[[y,y],x]} holds
ex q, r being set st [q,r] = p
proof end;

for q, r1, r2 being set st [q,r1] in {[[x,x],x],[[x,y],y],[[y,x],y],[[y,y],x]} & [q,r2] in {[[x,x],x],[[x,y],y],[[y,x],y],[[y,y],x]} holds
r1 = r2
proof end;

then reconsider od = {[[x,x],x],[[x,y],y],[[y,x],y],[[y,y],x]} as Function by Lm10, FUNCT_1:2;

for t being set holds
( t in [:A,A:] iff ex r being set st [t,r] in {[[x,x],x],[[x,y],y],[[y,x],y],[[y,y],x]} )
proof end;

then Lm11: [:A,A:] = dom od
by RELAT_1:def 4;

then Lm12: [x,x] in dom od
by Lm8;

Lm13: [[x,x],x] in od
by ENUMSET1:def 2;

then Lm14: od . x,x = x
by Lm12, FUNCT_1:def 4;

Lm15: [x,y] in dom od
by Lm8, Lm11;

Lm16: [[x,y],y] in od
by ENUMSET1:def 2;

then Lm17: od . [x,y] = y
by Lm15, FUNCT_1:def 4;

Lm18: [y,x] in dom od
by Lm8, Lm11;

Lm19: [[y,x],y] in od
by ENUMSET1:def 2;

then Lm20: od . [y,x] = y
by Lm18, FUNCT_1:def 4;

Lm21: [y,y] in dom od
by Lm8, Lm11;

[[y,y],x] in od
by ENUMSET1:def 2;

then Lm22: od . y,y = x
by Lm21, FUNCT_1:def 4;

then Lm23: for t being set st t in [:A,A:] holds
od . t in A
by Lm6, Lm7, Lm8, Lm14, Lm17, Lm20;

set s2 = [[x,y],x];

set s3 = [[y,x],x];

set s4 = [[y,y],y];

set D = {[[x,x],x],[[x,y],x],[[y,x],x],[[y,y],y]};

Lm24: for p being set st p in {[[x,x],x],[[x,y],x],[[y,x],x],[[y,y],y]} holds
ex q, r being set st [q,r] = p
proof end;

for q, r1, r2 being set st [q,r1] in {[[x,x],x],[[x,y],x],[[y,x],x],[[y,y],y]} & [q,r2] in {[[x,x],x],[[x,y],x],[[y,x],x],[[y,y],y]} holds
r1 = r2
proof end;

then reconsider om = {[[x,x],x],[[x,y],x],[[y,x],x],[[y,y],y]} as Function by Lm24, FUNCT_1:2;

for t being set holds
( t in [:A,A:] iff ex r being set st [t,r] in {[[x,x],x],[[x,y],x],[[y,x],x],[[y,y],y]} )
proof end;

then Lm25: [:A,A:] = dom om
by RELAT_1:def 4;

then Lm26: [x,x] in dom om
by Lm8;

[[x,x],x] in om
by ENUMSET1:def 2;

then Lm27: om . [x,x] = x
by Lm26, FUNCT_1:def 4;

Lm28: [x,y] in dom om
by Lm8, Lm25;

[[x,y],x] in om
by ENUMSET1:def 2;

then Lm29: om . [x,y] = x
by Lm28, FUNCT_1:def 4;

Lm30: [y,x] in dom om
by Lm8, Lm25;

[[y,x],x] in om
by ENUMSET1:def 2;

then Lm31: om . [y,x] = x
by Lm30, FUNCT_1:def 4;

Lm32: [y,y] in dom om
by Lm8, Lm25;

[[y,y],y] in om
by ENUMSET1:def 2;

then Lm33: om . [y,y] = y
by Lm32, FUNCT_1:def 4;

then Lm34: for t being set st t in [:A,A:] holds
om . t in A
by Lm6, Lm7, Lm8, Lm27, Lm29, Lm31;

then Lm35: om is BinOp of A
by Lm25, FUNCT_2:5;

Lm36: A \ {x} = {y}
by Lm5, ZFMISC_1:23;

then Lm37: [:(A \ {x}),(A \ {x}):] = {[y,y]}
by ZFMISC_1:35;

Lm38: for t being set st t in [:(A \ {x}),(A \ {x}):] holds
om . t in A \ {x}
proof end;

reconsider nm = y as Element of A \ {nd} by Lm36, TARSKI:def 1;

reconsider od0 = od as BinOp of A by Lm11, Lm23, FUNCT_2:5;

reconsider om0 = om as BinOp of A by Lm25, Lm34, FUNCT_2:5;

Lm39: for a, b, d being Element of A holds od0 . (od0 . a,b),d = od0 . a,(od0 . b,d)
proof end;

Lm40: for a being Element of A holds
( od0 . a,nd = a & od0 . nd,a = a )
proof end;

Lm41: for a being Element of A ex b being Element of A st
( od0 . a,b = nd & od0 . b,a = nd )
proof end;

for a, b being Element of A holds od0 . a,b = od0 . b,a
proof end;

then Lm42: LoopStr(# A,od0,nd #) is Group
by Def1, Def2, Def3, Def4, Lm39, Lm40, Lm41;

reconsider om1 = om as DnT of nd,A by Lm35, Lm38, REALSET1:def 8;

Lm43: for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm & P = om1 ! A,nd holds
LoopStr(# B,P,e #) is Group
proof end;

Lm44: for a, b, d being Element of A holds
( om0 . [a,(od0 . [b,d])] = od0 . [(om0 . [a,b]),(om0 . [a,d])] & om0 . [(od0 . [a,b]),d] = od0 . [(om0 . [a,d]),(om0 . [b,d])] )
proof end;

definition
let IT be doubleLoopStr ;
attr IT is Field-like means :Def8: :: REALSET2:def 8
 ex A being non trivial set ex od being BinOp of A ex nd being Element of A ex om being DnT of nd,A ex nm being Element of A \ {nd} st
( IT = field A,od,om,nd,nm & LoopStr(# A,od,nd #) is Group & ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm & P = om ! A,nd holds
LoopStr(# B,P,e #) is Group ) & ( for x, y, z being Element of A holds
( om . [x,(od . [y,z])] = od . [(om . [x,y]),(om . [x,z])] & om . [(od . [x,y]),z] = od . [(om . [x,z]),(om . [y,z])] ) ) );
end;

:: deftheorem Def8 defines Field-like REALSET2:def 8 :
for IT being doubleLoopStr holds
( IT is Field-like iff ex A being non trivial set ex od being BinOp of A ex nd being Element of A ex om being DnT of nd,A ex nm being Element of A \ {nd} st
( IT = field A,od,om,nd,nm & LoopStr(# A,od,nd #) is Group & ( for B being non empty set
for P being BinOp of B
for e being Element of B st B = A \ {nd} & e = nm & P = om ! A,nd holds
LoopStr(# B,P,e #) is Group ) & ( for x, y, z being Element of A holds
( om . [x,(od . [y,z])] = od . [(om . [x,y]),(om . [x,z])] & om . [(od . [x,y]),z] = od . [(om . [x,z]),(om . [y,z])] ) ) ) );

registration
cluster strict Field-like doubleLoopStr ;
existence
ex b1 being doubleLoopStr st
( b1 is strict & b1 is Field-like )
proof end;
end;

definition
mode Field is Field-like doubleLoopStr ;
end;

definition
let F be Field;
func suppf F -> non trivial set means :Def9: :: REALSET2:def 9
 ex od being BinOp of it ex nd being Element of it ex om being DnT of nd,it ex nm being Element of it \ {nd} st F = field it,od,om,nd,nm;
existence
ex b1 being non trivial set ex od being BinOp of b1 ex nd being Element of b1 ex om being DnT of nd,b1 ex nm being Element of b1 \ {nd} st F = field b1,od,om,nd,nm
proof end;
uniqueness
for b1, b2 being non trivial set st ex od being BinOp of b1 ex nd being Element of b1 ex om being DnT of nd,b1 ex nm being Element of b1 \ {nd} st F = field b1,od,om,nd,nm & ex od being BinOp of b2 ex nd being Element of b2 ex om being DnT of nd,b2 ex nm being Element of b2 \ {nd} st F = field b2,od,om,nd,nm holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines suppf REALSET2:def 9 :
for F being Field
for b2 being non trivial set holds
( b2 = suppf F iff ex od being BinOp of b2 ex nd being Element of b2 ex om being DnT of nd,b2 ex nm being Element of b2 \ {nd} st F = field b2,od,om,nd,nm );

definition
let F be Field;
func odf F -> BinOp of suppf F means :Def10: :: REALSET2:def 10
 ex nd being Element of suppf F ex om being DnT of nd, suppf F ex nm being Element of (suppf F) \ {nd} st F = field (suppf F),it,om,nd,nm;
existence
ex b1 being BinOp of suppf F ex nd being Element of suppf F ex om being DnT of nd, suppf F ex nm being Element of (suppf F) \ {nd} st F = field (suppf F),b1,om,nd,nm by Def9;
uniqueness
for b1, b2 being BinOp of suppf F st ex nd being Element of suppf F ex om being DnT of nd, suppf F ex nm being Element of (suppf F) \ {nd} st F = field (suppf F),b1,om,nd,nm & ex nd being Element of suppf F ex om being DnT of nd, suppf F ex nm being Element of (suppf F) \ {nd} st F = field (suppf F),b2,om,nd,nm holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines odf REALSET2:def 10 :
for F being Field
for b2 being BinOp of suppf F holds
( b2 = odf F iff ex nd being Element of suppf F ex om being DnT of nd, suppf F ex nm being Element of (suppf F) \ {nd} st F = field (suppf F),b2,om,nd,nm );

definition
let F be Field;
func ndf F -> Element of suppf F means :Def11: :: REALSET2:def 11
 ex om being DnT of it, suppf F ex nm being Element of (suppf F) \ {it} st F = field (suppf F),(odf F),om,it,nm;
existence
ex b1 being Element of suppf F ex om being DnT of b1, suppf F ex nm being Element of (suppf F) \ {b1} st F = field (suppf F),(odf F),om,b1,nm by Def10;
uniqueness
for b1, b2 being Element of suppf F st ex om being DnT of b1, suppf F ex nm being Element of (suppf F) \ {b1} st F = field (suppf F),(odf F),om,b1,nm & ex om being DnT of b2, suppf F ex nm being Element of (suppf F) \ {b2} st F = field (suppf F),(odf F),om,b2,nm holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines ndf REALSET2:def 11 :
for F being Field
for b2 being Element of suppf F holds
( b2 = ndf F iff ex om being DnT of b2, suppf F ex nm being Element of (suppf F) \ {b2} st F = field (suppf F),(odf F),om,b2,nm );

definition
let F be Field;
func omf F -> DnT of ndf F, suppf F means :Def12: :: REALSET2:def 12
 ex nm being Element of (suppf F) \ {(ndf F)} st F = field (suppf F),(odf F),it,(ndf F),nm;
existence
ex b1 being DnT of ndf F, suppf F ex nm being Element of (suppf F) \ {(ndf F)} st F = field (suppf F),(odf F),b1,(ndf F),nm by Def11;
uniqueness
for b1, b2 being DnT of ndf F, suppf F st ex nm being Element of (suppf F) \ {(ndf F)} st F = field (suppf F),(odf F),b1,(ndf F),nm & ex nm being Element of (suppf F) \ {(ndf F)} st F = field (suppf F),(odf F),b2,(ndf F),nm holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines omf REALSET2:def 12 :
for F being Field
for b2 being DnT of ndf F, suppf F holds
( b2 = omf F iff ex nm being Element of (suppf F) \ {(ndf F)} st F = field (suppf F),(odf F),b2,(ndf F),nm );

definition
let F be Field;
func nmf F -> Element of (suppf F) \ {(ndf F)} means :Def13: :: REALSET2:def 13
F = field (suppf F),(odf F),(omf F),(ndf F),it;
existence
ex b1 being Element of (suppf F) \ {(ndf F)} st F = field (suppf F),(odf F),(omf F),(ndf F),b1 by Def12;
uniqueness
for b1, b2 being Element of (suppf F) \ {(ndf F)} st F = field (suppf F),(odf F),(omf F),(ndf F),b1 & F = field (suppf F),(odf F),(omf F),(ndf F),b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines nmf REALSET2:def 13 :
for F being Field
for b2 being Element of (suppf F) \ {(ndf F)} holds
( b2 = nmf F iff F = field (suppf F),(odf F),(omf F),(ndf F),b2 );

theorem Th1: :: REALSET2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds LoopStr(# (suppf F),(odf F),(ndf F) #) is Group
proof end;

theorem Th2: :: REALSET2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for B being non empty set
for P being BinOp of B
for e being Element of B st B = (suppf F) \ {(ndf F)} & e = nmf F & P = (omf F) ! (suppf F),(ndf F) holds
LoopStr(# B,P,e #) is Group
proof end;

theorem Th3: :: REALSET2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for x, y, z being Element of suppf F holds
( (omf F) . [x,((odf F) . [y,z])] = (odf F) . [((omf F) . [x,y]),((omf F) . [x,z])] & (omf F) . [((odf F) . [x,y]),z] = (odf F) . [((omf F) . [x,z]),((omf F) . [y,z])] )
proof end;

theorem Th4: :: REALSET2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of suppf F holds (odf F) . ((odf F) . a,b),c = (odf F) . a,((odf F) . b,c)
proof end;

theorem Th5: :: REALSET2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b being Element of suppf F holds (odf F) . a,b = (odf F) . b,a
proof end;

theorem Th6: :: REALSET2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a being Element of suppf F holds
( (odf F) . a,(ndf F) = a & (odf F) . (ndf F),a = a )
proof end;

theorem Th7: :: REALSET2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a being Element of suppf F ex b being Element of suppf F st
( (odf F) . a,b = ndf F & (odf F) . b,a = ndf F )
proof end;

theorem Th8: :: REALSET2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of (suppf F) \ {(ndf F)} holds (omf F) . [((omf F) . [a,b]),c] = (omf F) . [a,((omf F) . [b,c])]
proof end;

theorem Th9: :: REALSET2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b being Element of (suppf F) \ {(ndf F)} holds (omf F) . [a,b] = (omf F) . [b,a]
proof end;

theorem Th10: :: REALSET2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a being Element of (suppf F) \ {(ndf F)} holds
( (omf F) . [a,(nmf F)] = a & (omf F) . [(nmf F),a] = a )
proof end;

theorem Th11: :: REALSET2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a being Element of (suppf F) \ {(ndf F)} ex b being Element of (suppf F) \ {(ndf F)} st
( (omf F) . [a,b] = nmf F & (omf F) . [b,a] = nmf F )
proof end;

definition
let F be Field;
func compf F -> Function of suppf F, suppf F means :Def14: :: REALSET2:def 14
for x being Element of suppf F holds (odf F) . [x,(it . x)] = ndf F;
existence
ex b1 being Function of suppf F, suppf F st
for x being Element of suppf F holds (odf F) . [x,(b1 . x)] = ndf F
proof end;
uniqueness
for b1, b2 being Function of suppf F, suppf F st ( for x being Element of suppf F holds (odf F) . [x,(b1 . x)] = ndf F ) & ( for x being Element of suppf F holds (odf F) . [x,(b2 . x)] = ndf F ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines compf REALSET2:def 14 :
for F being Field
for b2 being Function of suppf F, suppf F holds
( b2 = compf F iff for x being Element of suppf F holds (odf F) . [x,(b2 . x)] = ndf F );

theorem Th12: :: REALSET2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for x, y being Element of suppf F st (odf F) . x,y = ndf F holds
y = (compf F) . x
proof end;

theorem :: REALSET2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for x being Element of suppf F holds x = (compf F) . ((compf F) . x)
proof end;

theorem Th14: :: REALSET2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b being Element of suppf F holds
( (odf F) . [a,b] is Element of suppf F & (omf F) . [a,b] is Element of suppf F & (compf F) . a is Element of suppf F )
proof end;

theorem Th15: :: REALSET2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of suppf F holds (omf F) . [a,((odf F) . [b,((compf F) . c)])] = (odf F) . [((omf F) . [a,b]),((compf F) . ((omf F) . [a,c]))]
proof end;

theorem Th16: :: REALSET2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of suppf F holds (omf F) . [((odf F) . [a,((compf F) . b)]),c] = (odf F) . [((omf F) . [a,c]),((compf F) . ((omf F) . [b,c]))]
proof end;

theorem Th17: :: REALSET2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a being Element of suppf F holds (omf F) . [a,(ndf F)] = ndf F
proof end;

theorem Th18: :: REALSET2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a being Element of suppf F holds (omf F) . [(ndf F),a] = ndf F
proof end;

theorem :: REALSET2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b being Element of suppf F holds (compf F) . ((omf F) . [a,b]) = (omf F) . [a,((compf F) . b)]
proof end;

theorem Th20: :: REALSET2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds (omf F) . [(nmf F),(ndf F)] = ndf F
proof end;

theorem Th21: :: REALSET2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds (omf F) . [(ndf F),(nmf F)] = ndf F
proof end;

theorem :: REALSET2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b being Element of suppf F holds (omf F) . [a,b] is Element of suppf F by Th14;

theorem Th23: :: REALSET2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of suppf F holds (omf F) . [((omf F) . [a,b]),c] = (omf F) . [a,((omf F) . [b,c])]
proof end;

theorem :: REALSET2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b being Element of suppf F holds (omf F) . [a,b] = (omf F) . [b,a]
proof end;

theorem Th25: :: REALSET2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a being Element of suppf F holds
( (omf F) . [a,(nmf F)] = a & (omf F) . [(nmf F),a] = a )
proof end;

definition
let F be Field;
func revf F -> Function of (suppf F) \ {(ndf F)},(suppf F) \ {(ndf F)} means :Def15: :: REALSET2:def 15
for x being Element of (suppf F) \ {(ndf F)} holds (omf F) . [x,(it . x)] = nmf F;
existence
ex b1 being Function of (suppf F) \ {(ndf F)},(suppf F) \ {(ndf F)} st
for x being Element of (suppf F) \ {(ndf F)} holds (omf F) . [x,(b1 . x)] = nmf F
proof end;
uniqueness
for b1, b2 being Function of (suppf F) \ {(ndf F)},(suppf F) \ {(ndf F)} st ( for x being Element of (suppf F) \ {(ndf F)} holds (omf F) . [x,(b1 . x)] = nmf F ) & ( for x being Element of (suppf F) \ {(ndf F)} holds (omf F) . [x,(b2 . x)] = nmf F ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines revf REALSET2:def 15 :
for F being Field
for b2 being Function of (suppf F) \ {(ndf F)},(suppf F) \ {(ndf F)} holds
( b2 = revf F iff for x being Element of (suppf F) \ {(ndf F)} holds (omf F) . [x,(b2 . x)] = nmf F );

theorem :: REALSET2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for x, y being Element of (suppf F) \ {(ndf F)} st (omf F) . [x,y] = nmf F holds
y = (revf F) . x
proof end;

theorem :: REALSET2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for x being Element of (suppf F) \ {(ndf F)} holds x = (revf F) . ((revf F) . x)
proof end;

theorem :: REALSET2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b being Element of (suppf F) \ {(ndf F)} holds
( (omf F) . [a,b] is Element of (suppf F) \ {(ndf F)} & (revf F) . a is Element of (suppf F) \ {(ndf F)} )
proof end;

theorem :: REALSET2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of suppf F st (odf F) . a,b = (odf F) . a,c holds
b = c
proof end;

theorem :: REALSET2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a being Element of (suppf F) \ {(ndf F)}
for b, c being Element of suppf F st (omf F) . [a,b] = (omf F) . [a,c] holds
b = c
proof end;