:: REALSET3 semantic presentation

theorem Th1: :: REALSET3:1
for b1 being Field holds (compf b1) . (ndf b1) = ndf b1
proof end;

theorem Th2: :: REALSET3:2
for b1 being Field holds (revf b1) . (nmf b1) = nmf b1
proof end;

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

theorem Th4: :: REALSET3:4
for b1 being Field
for b2, b3 being Element of (suppf b1) \ {(ndf b1)} holds (revf b1) . ((omf b1) . [b2,((revf b1) . b3)]) = (omf b1) . [b3,((revf b1) . b2)]
proof end;

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

theorem Th6: :: REALSET3:6
for b1 being Field
for b2, b3 being Element of (suppf b1) \ {(ndf b1)} holds (revf b1) . ((omf b1) . [b2,b3]) = (omf b1) . [((revf b1) . b2),((revf b1) . b3)]
proof end;

theorem Th7: :: REALSET3:7
for b1 being Field
for b2, b3, b4, b5 being Element of suppf b1 holds
( (odf b1) . b2,((compf b1) . b3) = (odf b1) . [b4,((compf b1) . b5)] iff (odf b1) . [b2,b5] = (odf b1) . [b3,b4] )
proof end;

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

theorem Th9: :: REALSET3:9
for b1 being Field
for b2, b3 being Element of suppf b1 holds
( (omf b1) . [b2,b3] = ndf b1 iff ( b2 = ndf b1 or b3 = ndf b1 ) )
proof end;

theorem Th10: :: REALSET3:10
for b1 being Field
for b2, b3 being Element of suppf b1
for b4, b5 being Element of (suppf b1) \ {(ndf b1)} holds (omf b1) . [((omf b1) . [b2,((revf b1) . b4)]),((omf b1) . [b3,((revf b1) . b5)])] = (omf b1) . [((omf b1) . [b2,b3]),((revf b1) . ((omf b1) . [b4,b5]))]
proof end;

theorem Th11: :: REALSET3:11
for b1 being Field
for b2, b3 being Element of suppf b1
for b4, b5 being Element of (suppf b1) \ {(ndf b1)} holds (odf b1) . [((omf b1) . [b2,((revf b1) . b4)]),((omf b1) . [b3,((revf b1) . b5)])] = (omf b1) . [((odf b1) . [((omf b1) . [b2,b5]),((omf b1) . [b3,b4])]),((revf b1) . ((omf b1) . [b4,b5]))]
proof end;

definition
let c1 be Field;
func osf c1 -> BinOp of suppf a1 means :Def1: :: REALSET3:def 1
for b1, b2 being Element of suppf a1 holds a2 . [b1,b2] = (odf a1) . [b1,((compf a1) . b2)];
existence
ex b1 being BinOp of suppf c1 st
for b2, b3 being Element of suppf c1 holds b1 . [b2,b3] = (odf c1) . [b2,((compf c1) . b3)]
proof end;
uniqueness
for b1, b2 being BinOp of suppf c1 st ( for b3, b4 being Element of suppf c1 holds b1 . [b3,b4] = (odf c1) . [b3,((compf c1) . b4)] ) & ( for b3, b4 being Element of suppf c1 holds b2 . [b3,b4] = (odf c1) . [b3,((compf c1) . b4)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines osf REALSET3:def 1 :
for b1 being Field
for b2 being BinOp of suppf b1 holds
( b2 = osf b1 iff for b3, b4 being Element of suppf b1 holds b2 . [b3,b4] = (odf b1) . [b3,((compf b1) . b4)] );

theorem Th12: :: REALSET3:12
canceled;

theorem Th13: :: REALSET3:13
canceled;

theorem Th14: :: REALSET3:14
for b1 being Field
for b2 being Element of suppf b1 holds (osf b1) . [b2,b2] = ndf b1
proof end;

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

theorem Th16: :: REALSET3:16
for b1 being Field
for b2, b3 being Element of suppf b1 holds (osf b1) . [b2,b3] is Element of suppf b1
proof end;

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

theorem Th18: :: REALSET3:18
for b1 being Field
for b2, b3 being Element of suppf b1 holds (osf b1) . [b2,b3] = (compf b1) . ((osf b1) . [b3,b2])
proof end;

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

theorem Th20: :: REALSET3:20
for b1 being Field
for b2, b3, b4, b5 being Element of suppf b1 holds
( (osf b1) . [b2,b3] = (osf b1) . [b4,b5] iff (odf b1) . [b2,b5] = (odf b1) . [b3,b4] )
proof end;

theorem Th21: :: REALSET3:21
for b1 being Field
for b2 being Element of suppf b1 holds (osf b1) . [(ndf b1),b2] = (compf b1) . b2
proof end;

theorem Th22: :: REALSET3:22
for b1 being Field
for b2 being Element of suppf b1 holds (osf b1) . [b2,(ndf b1)] = b2
proof end;

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

theorem Th24: :: REALSET3:24
for b1 being Field
for b2, b3, b4 being Element of suppf b1 holds
( (odf b1) . [b2,b3] = b4 iff (osf b1) . [b4,b3] = b2 )
proof end;

theorem Th25: :: REALSET3:25
for b1 being Field
for b2, b3, b4 being Element of suppf b1 holds (osf b1) . [b2,((osf b1) . [b3,b4])] = (odf b1) . [((osf b1) . [b2,b3]),b4]
proof end;

theorem Th26: :: REALSET3:26
for b1 being Field
for b2, b3, b4 being Element of suppf b1 holds (osf b1) . [b2,((odf b1) . [b3,b4])] = (osf b1) . [((osf b1) . [b2,b3]),b4]
proof end;

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

:: deftheorem Def2 defines ovf REALSET3:def 2 :
for b1 being Field
for b2 being Function of [:(suppf b1),((suppf b1) \ {(ndf b1)}):], suppf b1 holds
( b2 = ovf b1 iff for b3 being Element of suppf b1
for b4 being Element of (suppf b1) \ {(ndf b1)} holds b2 . [b3,b4] = (omf b1) . [b3,((revf b1) . b4)] );

theorem Th27: :: REALSET3:27
canceled;

theorem Th28: :: REALSET3:28
canceled;

theorem Th29: :: REALSET3:29
for b1 being Field
for b2 being Element of (suppf b1) \ {(ndf b1)} holds (ovf b1) . [b2,b2] = nmf b1
proof end;

theorem Th30: :: REALSET3:30
for b1 being Field
for b2 being Element of suppf b1
for b3 being Element of (suppf b1) \ {(ndf b1)} holds (ovf b1) . [b2,b3] is Element of suppf b1
proof end;

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

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

theorem Th33: :: REALSET3:33
canceled;

theorem Th34: :: REALSET3:34
canceled;

theorem Th35: :: REALSET3:35
for b1 being Field
for b2, b3 being Element of (suppf b1) \ {(ndf b1)} holds (ovf b1) . [b2,b3] = (revf b1) . ((ovf b1) . [b3,b2])
proof end;

theorem Th36: :: REALSET3:36
for b1 being Field
for b2, b3 being Element of (suppf b1) \ {(ndf b1)} holds (ovf b1) . [((revf b1) . b2),b3] = (revf b1) . ((omf b1) . [b2,b3])
proof end;

theorem Th37: :: REALSET3:37
for b1 being Field
for b2, b3 being Element of suppf b1
for b4, b5 being Element of (suppf b1) \ {(ndf b1)} holds
( (ovf b1) . [b2,b4] = (ovf b1) . [b3,b5] iff (omf b1) . [b2,b5] = (omf b1) . [b4,b3] )
proof end;

theorem Th38: :: REALSET3:38
for b1 being Field
for b2 being Element of (suppf b1) \ {(ndf b1)} holds (ovf b1) . [(nmf b1),b2] = (revf b1) . b2
proof end;

theorem Th39: :: REALSET3:39
for b1 being Field
for b2 being Element of suppf b1 holds (ovf b1) . [b2,(nmf b1)] = b2
proof end;

theorem Th40: :: REALSET3:40
for b1 being Field
for b2 being Element of (suppf b1) \ {(ndf b1)}
for b3, b4 being Element of suppf b1 holds
( (omf b1) . [b2,b3] = b4 iff (ovf b1) . [b4,b2] = b3 )
proof end;

theorem Th41: :: REALSET3:41
for b1 being Field
for b2, b3 being Element of suppf b1
for b4 being Element of (suppf b1) \ {(ndf b1)} holds
( (omf b1) . [b2,b4] = b3 iff (ovf b1) . [b3,b4] = b2 )
proof end;

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

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