:: REALSET2 semantic presentation

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

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

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

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

:: deftheorem Def3 defines add-associative REALSET2:def 3 :
for b1 being non empty LoopStr holds
( b1 is add-associative iff for b2, b3, b4 being Element of b1 holds the add of b1 . (the add of b1 . b2,b3),b4 = the add of b1 . b2,(the add of b1 . b3,b4) );

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

E5: now
consider c1 being set ;
set c2 = {c1};
E6: c1 in {c1} by TARSKI:def 1;
consider c3 being BinOp of {c1};
E7: c3 . [c1,c1] = c1
proof
E8: ( dom c3 = [:{c1},{c1}:] & rng c3 c= {c1} ) by FUNCT_2:def 1, RELSET_1:12;
[c1,c1] in [:{c1},{c1}:] by E6, ZFMISC_1:def 2;
then c3 . [c1,c1] in rng c3 by E8, FUNCT_1:def 5;
hence c3 . [c1,c1] = c1 by E8, TARSKI:def 1;
end;
reconsider c4 = c1 as Element of {c1} by TARSKI:def 1;
E8: for b1, b2, b3 being Element of {c1} holds c3 . (c3 . b1,b2),b3 = c3 . b1,(c3 . b2,b3)
proof
let c5, c6, c7 be Element of {c1};
( c5 = c1 & c6 = c1 & c7 = c1 ) by TARSKI:def 1;
hence c3 . (c3 . c5,c6),c7 = c3 . c5,(c3 . c6,c7) by E7;
end;
E9: for b1 being Element of {c1} holds
( c3 . b1,c4 = b1 & c3 . c4,b1 = b1 )
proof
let c5 be Element of {c1};
c5 = c1 by TARSKI:def 1;
hence ( c3 . c5,c4 = c5 & c3 . c4,c5 = c5 ) by E7;
end;
E10: for b1 being Element of {c1} ex b2 being Element of {c1} st
( c3 . b1,b2 = c4 & c3 . b2,b1 = c4 )
proof
let c5 be Element of {c1};
take c4 ;
thus ( c3 . c5,c4 = c4 & c3 . c4,c5 = c4 ) by TARSKI:def 1;
end;
for b1, b2 being Element of {c1} holds c3 . b1,b2 = c3 . b2,b1
proof
let c5, c6 be Element of {c1};
( c5 = c1 & c6 = c1 ) by TARSKI:def 1;
hence c3 . c5,c6 = c3 . c6,c5 ;
end;
hence ex b1 being non empty set ex b2 being BinOp of b1ex b3 being Element of b1 st
( ( for b4, b5, b6 being Element of b1 holds b2 . (b2 . b4,b5),b6 = b2 . b4,(b2 . b5,b6) ) & ( for b4 being Element of b1 holds
( b2 . b4,b3 = b4 & b2 . b3,b4 = b4 ) ) & ( for b4 being Element of b1 ex b5 being Element of b1 st
( b2 . b4,b5 = b3 & b2 . b5,b4 = b3 ) ) & ( for b4, b5 being Element of b1 holds b2 . b4,b5 = b2 . b5,b4 ) ) by E8, E9, E10;
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 c1 be 1-sorted ;
attr a1 is trivial means :: REALSET2:def 5
the carrier of a1 is trivial;
end;

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

Lemma6: for b1 being 1-sorted holds
( b1 is trivial iff for b2, b3 being Element of b1 holds b2 = b3 )
proof end;

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

E7: now
let c1 be non trivial set ;
let c2, c3 be BinOp of c1;
let c4 be Element of c1;
let c5 be Element of c1 \ {c4};
let c6 be Element of c1;
assume E8: c6 = c5 ;
set c7 = doubleLoopStr(# c1,c2,c3,c6,c4 #);
thus not doubleLoopStr(# c1,c2,c3,c6,c4 #) is trivial
proof
now
take c8 = c4;
take c9 = c6;
not c5 in {c8} by XBOOLE_0:def 4;
hence c8 <> c9 by E8, TARSKI:def 1;
end;
hence not doubleLoopStr(# c1,c2,c3,c6,c4 #) is trivial by Lemma6;
end;
thus doubleLoopStr(# c1,c2,c3,c6,c4 #) is strict ;
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 c1 be non trivial set ;
let c2, c3 be BinOp of c1;
let c4 be Element of c1;
let c5 be Element of c1 \ {c4};
func field c1,c2,c3,c4,c5 -> strict non trivial doubleLoopStr means :Def6: :: REALSET2:def 6
( a1 = the carrier of a6 & a2 = the add of a6 & a3 = the mult of a6 & a4 = the Zero of a6 & a5 = the unity of a6 );
existence
ex b1 being strict non trivial doubleLoopStr st
( c1 = the carrier of b1 & c2 = the add of b1 & c3 = the mult of b1 & c4 = the Zero of b1 & c5 = the unity of b1 )
proof end;
uniqueness
for b1, b2 being strict non trivial doubleLoopStr st c1 = the carrier of b1 & c2 = the add of b1 & c3 = the mult of b1 & c4 = the Zero of b1 & c5 = the unity of b1 & c1 = the carrier of b2 & c2 = the add of b2 & c3 = the mult of b2 & c4 = the Zero of b2 & c5 = the unity of b2 holds
b1 = b2 ;
end;

:: deftheorem Def6 defines field REALSET2:def 6 :
for b1 being non trivial set
for b2, b3 being BinOp of b1
for b4 being Element of b1
for b5 being Element of b1 \ {b4}
for b6 being strict non trivial doubleLoopStr holds
( b6 = field b1,b2,b3,b4,b5 iff ( b1 = the carrier of b6 & b2 = the add of b6 & b3 = the mult of b6 & b4 = the Zero of b6 & b5 = the unity of b6 ) );

definition
let c1 be 1-sorted ;
redefine attr a1 is trivial means :: REALSET2:def 7
for b1, b2 being Element of a1 holds b1 = b2;
compatibility
( c1 is trivial iff for b1, b2 being Element of c1 holds b1 = b2 ) by Lemma6;
end;

:: deftheorem Def7 defines trivial REALSET2:def 7 :
for b1 being 1-sorted holds
( b1 is trivial iff for b2, b3 being Element of b1 holds b2 = b3 );

consider c1, c2 being set such that
Lemma9: c1 <> c2 by VECTSP_1:78;

set c3 = {c1,c2};

Lemma10: c1 in {c1,c2}
by TARSKI:def 2;

Lemma11: c2 in {c1,c2}
by TARSKI:def 2;

for b1 being Element of {c1,c2} holds {c1,c2} \ {b1} is non empty set
proof end;

then reconsider c4 = {c1,c2} as non trivial set by REALSET1:6;

reconsider c5 = c1 as Element of c4 by TARSKI:def 2;

Lemma12: for b1 being set holds
( b1 in [:c4,c4:] iff ( b1 = [c1,c1] or b1 = [c1,c2] or b1 = [c2,c1] or b1 = [c2,c2] ) )
proof end;

for b1 being set holds
( b1 in [:c4,c4:] iff b1 in {[c1,c1],[c1,c2],[c2,c1],[c2,c2]} )
by Lemma12, ENUMSET1:def 2;

Lemma13: [:c4,c4:] = {[c1,c1],[c1,c2],[c2,c1],[c2,c2]}
by Lemma12, ENUMSET1:def 2;

set c6 = [[c1,c1],c1];

set c7 = [[c1,c2],c2];

set c8 = [[c2,c1],c2];

set c9 = [[c2,c2],c1];

set c10 = {[[c1,c1],c1],[[c1,c2],c2],[[c2,c1],c2],[[c2,c2],c1]};

Lemma14: for b1 being set st b1 in {[[c1,c1],c1],[[c1,c2],c2],[[c2,c1],c2],[[c2,c2],c1]} holds
ex b2, b3 being set st [b2,b3] = b1
proof end;

for b1, b2, b3 being set st [b1,b2] in {[[c1,c1],c1],[[c1,c2],c2],[[c2,c1],c2],[[c2,c2],c1]} & [b1,b3] in {[[c1,c1],c1],[[c1,c2],c2],[[c2,c1],c2],[[c2,c2],c1]} holds
b2 = b3
proof end;

then reconsider c11 = {[[c1,c1],c1],[[c1,c2],c2],[[c2,c1],c2],[[c2,c2],c1]} as Function by Lemma14, FUNCT_1:2;

for b1 being set holds
( b1 in [:c4,c4:] iff ex b2 being set st [b1,b2] in {[[c1,c1],c1],[[c1,c2],c2],[[c2,c1],c2],[[c2,c2],c1]} )
proof end;

then Lemma15: [:c4,c4:] = dom c11
by RELAT_1:def 4;

then Lemma16: [c1,c1] in dom c11
by Lemma12;

Lemma17: [[c1,c1],c1] in c11
by ENUMSET1:def 2;

then Lemma18: c11 . c1,c1 = c1
by Lemma16, FUNCT_1:def 4;

Lemma19: [c1,c2] in dom c11
by Lemma12, Lemma15;

Lemma20: [[c1,c2],c2] in c11
by ENUMSET1:def 2;

then Lemma21: c11 . [c1,c2] = c2
by Lemma19, FUNCT_1:def 4;

Lemma22: [c2,c1] in dom c11
by Lemma12, Lemma15;

Lemma23: [[c2,c1],c2] in c11
by ENUMSET1:def 2;

then Lemma24: c11 . [c2,c1] = c2
by Lemma22, FUNCT_1:def 4;

Lemma25: [c2,c2] in dom c11
by Lemma12, Lemma15;

[[c2,c2],c1] in c11
by ENUMSET1:def 2;

then Lemma26: c11 . c2,c2 = c1
by Lemma25, FUNCT_1:def 4;

then Lemma27: for b1 being set st b1 in [:c4,c4:] holds
c11 . b1 in c4
by Lemma10, Lemma11, Lemma12, Lemma18, Lemma21, Lemma24;

set c12 = [[c1,c2],c1];

set c13 = [[c2,c1],c1];

set c14 = [[c2,c2],c2];

set c15 = {[[c1,c1],c1],[[c1,c2],c1],[[c2,c1],c1],[[c2,c2],c2]};

Lemma28: for b1 being set st b1 in {[[c1,c1],c1],[[c1,c2],c1],[[c2,c1],c1],[[c2,c2],c2]} holds
ex b2, b3 being set st [b2,b3] = b1
proof end;

for b1, b2, b3 being set st [b1,b2] in {[[c1,c1],c1],[[c1,c2],c1],[[c2,c1],c1],[[c2,c2],c2]} & [b1,b3] in {[[c1,c1],c1],[[c1,c2],c1],[[c2,c1],c1],[[c2,c2],c2]} holds
b2 = b3
proof end;

then reconsider c16 = {[[c1,c1],c1],[[c1,c2],c1],[[c2,c1],c1],[[c2,c2],c2]} as Function by Lemma28, FUNCT_1:2;

for b1 being set holds
( b1 in [:c4,c4:] iff ex b2 being set st [b1,b2] in {[[c1,c1],c1],[[c1,c2],c1],[[c2,c1],c1],[[c2,c2],c2]} )
proof end;

then Lemma29: [:c4,c4:] = dom c16
by RELAT_1:def 4;

then Lemma30: [c1,c1] in dom c16
by Lemma12;

[[c1,c1],c1] in c16
by ENUMSET1:def 2;

then Lemma31: c16 . [c1,c1] = c1
by Lemma30, FUNCT_1:def 4;

Lemma32: [c1,c2] in dom c16
by Lemma12, Lemma29;

[[c1,c2],c1] in c16
by ENUMSET1:def 2;

then Lemma33: c16 . [c1,c2] = c1
by Lemma32, FUNCT_1:def 4;

Lemma34: [c2,c1] in dom c16
by Lemma12, Lemma29;

[[c2,c1],c1] in c16
by ENUMSET1:def 2;

then Lemma35: c16 . [c2,c1] = c1
by Lemma34, FUNCT_1:def 4;

Lemma36: [c2,c2] in dom c16
by Lemma12, Lemma29;

[[c2,c2],c2] in c16
by ENUMSET1:def 2;

then Lemma37: c16 . [c2,c2] = c2
by Lemma36, FUNCT_1:def 4;

then Lemma38: for b1 being set st b1 in [:c4,c4:] holds
c16 . b1 in c4
by Lemma10, Lemma11, Lemma12, Lemma31, Lemma33, Lemma35;

then Lemma39: c16 is BinOp of c4
by Lemma29, FUNCT_2:5;

Lemma40: c4 \ {c1} = {c2}
by Lemma9, ZFMISC_1:23;

then Lemma41: [:(c4 \ {c1}),(c4 \ {c1}):] = {[c2,c2]}
by ZFMISC_1:35;

Lemma42: for b1 being set st b1 in [:(c4 \ {c1}),(c4 \ {c1}):] holds
c16 . b1 in c4 \ {c1}
proof end;

reconsider c17 = c2 as Element of c4 \ {c5} by Lemma40, TARSKI:def 1;

reconsider c18 = c11 as BinOp of c4 by Lemma15, Lemma27, FUNCT_2:5;

reconsider c19 = c16 as BinOp of c4 by Lemma29, Lemma38, FUNCT_2:5;

Lemma43: for b1, b2, b3 being Element of c4 holds c18 . (c18 . b1,b2),b3 = c18 . b1,(c18 . b2,b3)
proof end;

Lemma44: for b1 being Element of c4 holds
( c18 . b1,c5 = b1 & c18 . c5,b1 = b1 )
proof end;

Lemma45: for b1 being Element of c4 ex b2 being Element of c4 st
( c18 . b1,b2 = c5 & c18 . b2,b1 = c5 )
proof end;

for b1, b2 being Element of c4 holds c18 . b1,b2 = c18 . b2,b1
proof end;

then Lemma46: LoopStr(# c4,c18,c5 #) is Group
by Def1, Def2, Def3, Def4, Lemma43, Lemma44, Lemma45;

reconsider c20 = c16 as DnT of c5,c4 by Lemma39, Lemma42, REALSET1:def 8;

Lemma47: for b1 being non empty set
for b2 being BinOp of b1
for b3 being Element of b1 st b1 = c4 \ {c5} & b3 = c17 & b2 = c20 ! c4,c5 holds
LoopStr(# b1,b2,b3 #) is Group
proof end;

Lemma48: for b1, b2, b3 being Element of c4 holds
( c19 . [b1,(c18 . [b2,b3])] = c18 . [(c19 . [b1,b2]),(c19 . [b1,b3])] & c19 . [(c18 . [b1,b2]),b3] = c18 . [(c19 . [b1,b3]),(c19 . [b2,b3])] )
proof end;

definition
let c21 be doubleLoopStr ;
attr a1 is Field-like means :Def8: :: REALSET2:def 8
ex b1 being non trivial set ex b2 being BinOp of b1ex b3 being Element of b1ex b4 being DnT of b3,b1ex b5 being Element of b1 \ {b3} st
( a1 = field b1,b2,b4,b3,b5 & LoopStr(# b1,b2,b3 #) is Group & ( for b6 being non empty set
for b7 being BinOp of b6
for b8 being Element of b6 st b6 = b1 \ {b3} & b8 = b5 & b7 = b4 ! b1,b3 holds
LoopStr(# b6,b7,b8 #) is Group ) & ( for b6, b7, b8 being Element of b1 holds
( b4 . [b6,(b2 . [b7,b8])] = b2 . [(b4 . [b6,b7]),(b4 . [b6,b8])] & b4 . [(b2 . [b6,b7]),b8] = b2 . [(b4 . [b6,b8]),(b4 . [b7,b8])] ) ) );
end;

:: deftheorem Def8 defines Field-like REALSET2:def 8 :
for b1 being doubleLoopStr holds
( b1 is Field-like iff ex b2 being non trivial set ex b3 being BinOp of b2ex b4 being Element of b2ex b5 being DnT of b4,b2ex b6 being Element of b2 \ {b4} st
( b1 = field b2,b3,b5,b4,b6 & LoopStr(# b2,b3,b4 #) is Group & ( for b7 being non empty set
for b8 being BinOp of b7
for b9 being Element of b7 st b7 = b2 \ {b4} & b9 = b6 & b8 = b5 ! b2,b4 holds
LoopStr(# b7,b8,b9 #) is Group ) & ( for b7, b8, b9 being Element of b2 holds
( b5 . [b7,(b3 . [b8,b9])] = b3 . [(b5 . [b7,b8]),(b5 . [b7,b9])] & b5 . [(b3 . [b7,b8]),b9] = b3 . [(b5 . [b7,b9]),(b5 . [b8,b9])] ) ) ) );

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 c21 be Field;
func suppf c1 -> non trivial set means :Def9: :: REALSET2:def 9
ex b1 being BinOp of a2ex b2 being Element of a2ex b3 being DnT of b2,a2ex b4 being Element of a2 \ {b2} st a1 = field a2,b1,b3,b2,b4;
existence
ex b1 being non trivial set ex b2 being BinOp of b1ex b3 being Element of b1ex b4 being DnT of b3,b1ex b5 being Element of b1 \ {b3} st c21 = field b1,b2,b4,b3,b5
proof end;
uniqueness
for b1, b2 being non trivial set st ex b3 being BinOp of b1ex b4 being Element of b1ex b5 being DnT of b4,b1ex b6 being Element of b1 \ {b4} st c21 = field b1,b3,b5,b4,b6 & ex b3 being BinOp of b2ex b4 being Element of b2ex b5 being DnT of b4,b2ex b6 being Element of b2 \ {b4} st c21 = field b2,b3,b5,b4,b6 holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines suppf REALSET2:def 9 :
for b1 being Field
for b2 being non trivial set holds
( b2 = suppf b1 iff ex b3 being BinOp of b2ex b4 being Element of b2ex b5 being DnT of b4,b2ex b6 being Element of b2 \ {b4} st b1 = field b2,b3,b5,b4,b6 );

definition
let c21 be Field;
func odf c1 -> BinOp of suppf a1 means :Def10: :: REALSET2:def 10
ex b1 being Element of suppf a1ex b2 being DnT of b1, suppf a1ex b3 being Element of (suppf a1) \ {b1} st a1 = field (suppf a1),a2,b2,b1,b3;
existence
ex b1 being BinOp of suppf c21ex b2 being Element of suppf c21ex b3 being DnT of b2, suppf c21ex b4 being Element of (suppf c21) \ {b2} st c21 = field (suppf c21),b1,b3,b2,b4 by Def9;
uniqueness
for b1, b2 being BinOp of suppf c21 st ex b3 being Element of suppf c21ex b4 being DnT of b3, suppf c21ex b5 being Element of (suppf c21) \ {b3} st c21 = field (suppf c21),b1,b4,b3,b5 & ex b3 being Element of suppf c21ex b4 being DnT of b3, suppf c21ex b5 being Element of (suppf c21) \ {b3} st c21 = field (suppf c21),b2,b4,b3,b5 holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines odf REALSET2:def 10 :
for b1 being Field
for b2 being BinOp of suppf b1 holds
( b2 = odf b1 iff ex b3 being Element of suppf b1ex b4 being DnT of b3, suppf b1ex b5 being Element of (suppf b1) \ {b3} st b1 = field (suppf b1),b2,b4,b3,b5 );

definition
let c21 be Field;
func ndf c1 -> Element of suppf a1 means :Def11: :: REALSET2:def 11
ex b1 being DnT of a2, suppf a1ex b2 being Element of (suppf a1) \ {a2} st a1 = field (suppf a1),(odf a1),b1,a2,b2;
existence
ex b1 being Element of suppf c21ex b2 being DnT of b1, suppf c21ex b3 being Element of (suppf c21) \ {b1} st c21 = field (suppf c21),(odf c21),b2,b1,b3 by Def10;
uniqueness
for b1, b2 being Element of suppf c21 st ex b3 being DnT of b1, suppf c21ex b4 being Element of (suppf c21) \ {b1} st c21 = field (suppf c21),(odf c21),b3,b1,b4 & ex b3 being DnT of b2, suppf c21ex b4 being Element of (suppf c21) \ {b2} st c21 = field (suppf c21),(odf c21),b3,b2,b4 holds
b1 = b2
proof end;
end;

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

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

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

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

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

theorem Th1: :: REALSET2:1
for b1 being Field holds LoopStr(# (suppf b1),(odf b1),(ndf b1) #) is Group
proof end;

theorem Th2: :: REALSET2:2
for b1 being Field
for b2 being non empty set
for b3 being BinOp of b2
for b4 being Element of b2 st b2 = (suppf b1) \ {(ndf b1)} & b4 = nmf b1 & b3 = (omf b1) ! (suppf b1),(ndf b1) holds
LoopStr(# b2,b3,b4 #) is Group
proof end;

theorem Th3: :: REALSET2:3
for b1 being Field
for b2, b3, b4 being Element of suppf b1 holds
( (omf b1) . [b2,((odf b1) . [b3,b4])] = (odf b1) . [((omf b1) . [b2,b3]),((omf b1) . [b2,b4])] & (omf b1) . [((odf b1) . [b2,b3]),b4] = (odf b1) . [((omf b1) . [b2,b4]),((omf b1) . [b3,b4])] )
proof end;

theorem Th4: :: REALSET2:4
for b1 being Field
for b2, b3, b4 being Element of suppf b1 holds (odf b1) . ((odf b1) . b2,b3),b4 = (odf b1) . b2,((odf b1) . b3,b4)
proof end;

theorem Th5: :: REALSET2:5
for b1 being Field
for b2, b3 being Element of suppf b1 holds (odf b1) . b2,b3 = (odf b1) . b3,b2
proof end;

theorem Th6: :: REALSET2:6
for b1 being Field
for b2 being Element of suppf b1 holds
( (odf b1) . b2,(ndf b1) = b2 & (odf b1) . (ndf b1),b2 = b2 )
proof end;

theorem Th7: :: REALSET2:7
for b1 being Field
for b2 being Element of suppf b1 ex b3 being Element of suppf b1 st
( (odf b1) . b2,b3 = ndf b1 & (odf b1) . b3,b2 = ndf b1 )
proof end;

theorem Th8: :: REALSET2:8
for b1 being Field
for b2, b3, b4 being Element of (suppf b1) \ {(ndf b1)} holds (omf b1) . [((omf b1) . [b2,b3]),b4] = (omf b1) . [b2,((omf b1) . [b3,b4])]
proof end;

theorem Th9: :: REALSET2:9
for b1 being Field
for b2, b3 being Element of (suppf b1) \ {(ndf b1)} holds (omf b1) . [b2,b3] = (omf b1) . [b3,b2]
proof end;

theorem Th10: :: REALSET2:10
for b1 being Field
for b2 being Element of (suppf b1) \ {(ndf b1)} holds
( (omf b1) . [b2,(nmf b1)] = b2 & (omf b1) . [(nmf b1),b2] = b2 )
proof end;

theorem Th11: :: REALSET2:11
for b1 being Field
for b2 being Element of (suppf b1) \ {(ndf b1)} ex b3 being Element of (suppf b1) \ {(ndf b1)} st
( (omf b1) . [b2,b3] = nmf b1 & (omf b1) . [b3,b2] = nmf b1 )
proof end;

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

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

theorem Th12: :: REALSET2:12
for b1 being Field
for b2, b3 being Element of suppf b1 st (odf b1) . b2,b3 = ndf b1 holds
b3 = (compf b1) . b2
proof end;

theorem Th13: :: REALSET2:13
for b1 being Field
for b2 being Element of suppf b1 holds b2 = (compf b1) . ((compf b1) . b2)
proof end;

theorem Th14: :: REALSET2:14
for b1 being Field
for b2, b3 being Element of suppf b1 holds
( (odf b1) . [b2,b3] is Element of suppf b1 & (omf b1) . [b2,b3] is Element of suppf b1 & (compf b1) . b2 is Element of suppf b1 )
proof end;

theorem Th15: :: REALSET2:15
for b1 being Field
for b2, b3, b4 being Element of suppf b1 holds (omf b1) . [b2,((odf b1) . [b3,((compf b1) . b4)])] = (odf b1) . [((omf b1) . [b2,b3]),((compf b1) . ((omf b1) . [b2,b4]))]
proof end;

theorem Th16: :: REALSET2:16
for b1 being Field
for b2, b3, b4 being Element of suppf b1 holds (omf b1) . [((odf b1) . [b2,((compf b1) . b3)]),b4] = (odf b1) . [((omf b1) . [b2,b4]),((compf b1) . ((omf b1) . [b3,b4]))]
proof end;

theorem Th17: :: REALSET2:17
for b1 being Field
for b2 being Element of suppf b1 holds (omf b1) . [b2,(ndf b1)] = ndf b1
proof end;

theorem Th18: :: REALSET2:18
for b1 being Field
for b2 being Element of suppf b1 holds (omf b1) . [(ndf b1),b2] = ndf b1
proof end;

theorem Th19: :: REALSET2:19
for b1 being Field
for b2, b3 being Element of suppf b1 holds (compf b1) . ((omf b1) . [b2,b3]) = (omf b1) . [b2,((compf b1) . b3)]
proof end;

theorem Th20: :: REALSET2:20
for b1 being Field holds (omf b1) . [(nmf b1),(ndf b1)] = ndf b1
proof end;

theorem Th21: :: REALSET2:21
for b1 being Field holds (omf b1) . [(ndf b1),(nmf b1)] = ndf b1
proof end;

theorem Th22: :: REALSET2:22
for b1 being Field
for b2, b3 being Element of suppf b1 holds (omf b1) . [b2,b3] is Element of suppf b1 by Th14;

theorem Th23: :: REALSET2:23
for b1 being Field
for b2, b3, b4 being Element of suppf b1 holds (omf b1) . [((omf b1) . [b2,b3]),b4] = (omf b1) . [b2,((omf b1) . [b3,b4])]
proof end;

theorem Th24: :: REALSET2:24
for b1 being Field
for b2, b3 being Element of suppf b1 holds (omf b1) . [b2,b3] = (omf b1) . [b3,b2]
proof end;

theorem Th25: :: REALSET2:25
for b1 being Field
for b2 being Element of suppf b1 holds
( (omf b1) . [b2,(nmf b1)] = b2 & (omf b1) . [(nmf b1),b2] = b2 )
proof end;

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

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

theorem Th26: :: REALSET2:26
for b1 being Field
for b2, b3 being Element of (suppf b1) \ {(ndf b1)} st (omf b1) . [b2,b3] = nmf b1 holds
b3 = (revf b1) . b2
proof end;

theorem Th27: :: REALSET2:27
for b1 being Field
for b2 being Element of (suppf b1) \ {(ndf b1)} holds b2 = (revf b1) . ((revf b1) . b2)
proof end;

theorem Th28: :: REALSET2:28
for b1 being Field
for b2, b3 being Element of (suppf b1) \ {(ndf b1)} holds
( (omf b1) . [b2,b3] is Element of (suppf b1) \ {(ndf b1)} & (revf b1) . b2 is Element of (suppf b1) \ {(ndf b1)} )
proof end;

theorem Th29: :: REALSET2:29
for b1 being Field
for b2, b3, b4 being Element of suppf b1 st (odf b1) . b2,b3 = (odf b1) . b2,b4 holds
b3 = b4
proof end;

theorem Th30: :: REALSET2:30
for b1 being Field
for b2 being Element of (suppf b1) \ {(ndf b1)}
for b3, b4 being Element of suppf b1 st (omf b1) . [b2,b3] = (omf b1) . [b2,b4] holds
b3 = b4
proof end;