:: REALSET3 semantic presentation

begin

theorem Th1: :: REALSET3:1
for F being Field holds (revf F) . (1. F) = 1. F
proof
let F be Field; ::_thesis: (revf F) . (1. F) = 1. F
A1: 1. F is Element of NonZero F by STRUCT_0:2;
then  (1. F) * (1. F) = 1. F by REALSET2:6;
hence  (revf F) . (1. F) = 1. F by A1, REALSET2:22; ::_thesis: verum
end;

theorem Th2: :: REALSET3:2
for F being Field
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; ::_thesis: for a, b being Element of NonZero F holds (revf F) . ((omf F) . (a,((revf F) . b))) = (omf F) . (b,((revf F) . a))
let a, b be Element of NonZero F; ::_thesis: (revf F) . ((omf F) . (a,((revf F) . b))) = (omf F) . (b,((revf F) . a))
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  (revf F) . ((omf F) . (a,((revf F) . b))) = (omf F) . (b,((revf F) . a)) by A1, A2, REALSET2:22; ::_thesis: verum
end;

theorem Th3: :: REALSET3:3
for F being Field
for 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; ::_thesis: for a, b being Element of NonZero F holds (revf F) . ((omf F) . (a,b)) = (omf F) . (((revf F) . a),((revf F) . b))
let a, b be Element of NonZero F; ::_thesis: (revf F) . ((omf F) . (a,b)) = (omf F) . (((revf F) . a),((revf F) . b))
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)) ; ::_thesis: verum
end;

theorem Th4: :: REALSET3:4
for F being Field
for a, b, c, d being Element of F holds
( a - b = c - d iff a + d = b + c )
proof
let F be Field; ::_thesis: for a, b, c, d being Element of F holds
( a - b = c - d iff a + d = b + c )
let a, b, c, d be Element of F; ::_thesis: ( a - b = c - d iff a + d = b + c )
hereby  ::_thesis: ( a + d = b + c implies a - b = c - d )
assume  a - b = c - d ; ::_thesis: a + d = b + c
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 ;
::_thesis: verum
end;
assume  a + d = b + c ; ::_thesis: a - b = c - d
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 ;
::_thesis: verum
end;

theorem Th5: :: REALSET3:5
for F being Field
for a, c being Element of F
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; ::_thesis: for a, c being Element of F
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) )
let a, c be Element of F; ::_thesis: 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) )
let b, d be Element of NonZero F; ::_thesis: ( (omf F) . (a,((revf F) . b)) = (omf F) . (c,((revf F) . d)) iff (omf F) . (a,d) = (omf F) . (b,c) )
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)) ; ::_thesis: (omf F) . (a,d) = (omf F) . (b,c)
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 ;
::_thesis: verum
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) ; ::_thesis: (omf F) . (a,((revf F) . b)) = (omf F) . (c,((revf F) . d))
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 ;
::_thesis: verum
end;
hence  ( (omf F) . (a,((revf F) . b)) = (omf F) . (c,((revf F) . d)) iff (omf F) . (a,d) = (omf F) . (b,c) ) by A1; ::_thesis: verum
end;

theorem :: REALSET3:6
for F being Field
for a, b being Element of F
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; ::_thesis: for a, b being Element of F
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))))
let a, b be Element of F; ::_thesis: 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))))
let c, d be Element of NonZero F; ::_thesis: (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))))
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)))) ; ::_thesis: verum
end;

theorem :: REALSET3:7
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))))
proof
let F be Field; ::_thesis: 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))))
let a, b be Element of F; ::_thesis: 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))))
let c, d be Element of NonZero F; ::_thesis: 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))))
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)))) ;
::_thesis: verum
end;

definition
let F be Field;
func osf F ->  BinOp of the carrier of F means :Def1: :: REALSET3:def 1
 for x, y being Element of F holds it . (x,y) = the addF of F . (x,((comp F) . y));
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))
proof
defpred S1[ Element of F, Element of F, set ] means $3 = the addF of F . ($1,((comp F) . $2));
A1: for x, y being Element of F ex z being Element of F st S1[x,y,z] ;
 ex f being BinOp of the carrier of F st
for x, y being Element of F holds S1[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 ; ::_thesis: for x, y being Element of F holds S . (x,y) = the addF of F . (x,((comp F) . y))
thus  for x, y being Element of F holds S . (x,y) = the addF of F . (x,((comp F) . y)) by A2; ::_thesis: verum
end;
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
proof
let S1, S2 be BinOp of the carrier of F; ::_thesis: ( ( for x, y being Element of F holds S1 . (x,y) = the addF of F . (x,((comp F) . y)) ) & ( for x, y being Element of F holds S2 . (x,y) = the addF of F . (x,((comp F) . y)) ) implies S1 = S2 )
assume 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)) ; ::_thesis: S1 = S2
now__::_thesis:_for_p_being_set_st_p_in_[:_the_carrier_of_F,_the_carrier_of_F:]_holds_
S1_._p_=_S2_._p
let p be set ; ::_thesis: ( p in [: the carrier of F, the carrier of F:] implies S1 . p = S2 . p )
assume  p in [: the carrier of F, the carrier of F:] ; ::_thesis: S1 . p = S2 . p
then consider x, y being set  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 ; ::_thesis: verum
end;
hence  S1 = S2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines osf REALSET3:def_1_:_
 for F being Field
for b2 being BinOp of the carrier of F holds
( b2 = osf F iff for x, y being Element of F holds b2 . (x,y) = the addF of F . (x,((comp F) . y)) );

theorem :: REALSET3:8
for F being Field
for x being Element of F holds (osf F) . (x,x) = 0. F
proof
let F be Field; ::_thesis: for x being Element of F holds (osf F) . (x,x) = 0. F
let x be Element of F; ::_thesis: (osf F) . (x,x) = 0. 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 ; ::_thesis: verum
end;

theorem Th9: :: REALSET3:9
for F being Field
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; ::_thesis: 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)))
let a, b, c be Element of F; ::_thesis: (omf F) . (a,((osf F) . (b,c))) = (osf F) . (((omf F) . (a,b)),((omf F) . (a,c)))
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 ; ::_thesis: verum
end;

theorem :: REALSET3:10
for F being Field
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; ::_thesis: 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)))
let a, b, c be Element of F; ::_thesis: (omf F) . (((osf F) . (a,b)),c) = (osf F) . (((omf F) . (a,c)),((omf F) . (b,c)))
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))) ; ::_thesis: verum
end;

theorem :: REALSET3:11
for F being Field
for a, b being Element of F holds (osf F) . (a,b) = (comp F) . ((osf F) . (b,a))
proof
let F be Field; ::_thesis: for a, b being Element of F holds (osf F) . (a,b) = (comp F) . ((osf F) . (b,a))
let a, b be Element of F; ::_thesis: (osf F) . (a,b) = (comp F) . ((osf F) . (b,a))
(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  (osf F) . (a,b) = (comp F) . ((osf F) . (b,a)) by Def1; ::_thesis: verum
end;

theorem :: REALSET3:12
for F being Field
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; ::_thesis: for a, b being Element of F holds (osf F) . (((comp F) . a),b) = (comp F) . ( the addF of F . (a,b))
let a, b be Element of F; ::_thesis: (osf F) . (((comp F) . a),b) = (comp F) . ( the addF of F . (a,b))
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 ; ::_thesis: verum
end;

theorem Th13: :: REALSET3:13
for F being Field
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; ::_thesis: for a, b, c, d being Element of F holds
( (osf F) . (a,b) = (osf F) . (c,d) iff a + d = b + c )
let a, b, c, d be Element of F; ::_thesis: ( (osf F) . (a,b) = (osf F) . (c,d) iff a + d = b + c )
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  ( (osf F) . (a,b) = (osf F) . (c,d) iff a + d = b + c ) by A1, Th4; ::_thesis: verum
end;

theorem :: REALSET3:14
for F being Field
for a being Element of F holds (osf F) . ((0. F),a) = (comp F) . a
proof
let F be Field; ::_thesis: for a being Element of F holds (osf F) . ((0. F),a) = (comp F) . a
let a be Element of F; ::_thesis: (osf F) . ((0. F),a) = (comp F) . a
thus (osf F) . ((0. F),a) = (0. F) + ((comp F) . a) by Def1
.= (comp F) . a by REALSET2:2 ; ::_thesis: verum
end;

theorem Th15: :: REALSET3:15
for F being Field
for a being Element of F holds (osf F) . (a,(0. F)) = a
proof
let F be Field; ::_thesis: for a being Element of F holds (osf F) . (a,(0. F)) = a
let a be Element of F; ::_thesis: (osf F) . (a,(0. F)) = a
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 ; ::_thesis: verum
end;

theorem :: REALSET3:16
for F being Field
for a, b, c being Element of F holds
( a + b = c iff (osf F) . (c,a) = b )
proof
let F be Field; ::_thesis: for a, b, c being Element of F holds
( a + b = c iff (osf F) . (c,a) = b )
let a, b, c be Element of F; ::_thesis: ( a + b = c iff (osf F) . (c,a) = b )
set d = 0. F;
 ( c + (0. F) = c & (osf F) . (b,(0. F)) = b ) by Th15, REALSET2:2;
hence  ( a + b = c iff (osf F) . (c,a) = b ) by Th13; ::_thesis: verum
end;

theorem :: REALSET3:17
for F being Field
for a, b, c being Element of F holds
( a + b = c iff (osf F) . (c,b) = a )
proof
let F be Field; ::_thesis: for a, b, c being Element of F holds
( a + b = c iff (osf F) . (c,b) = a )
let a, b, c be Element of F; ::_thesis: ( a + b = c iff (osf F) . (c,b) = a )
set d = 0. F;
 ( c + (0. F) = c & (osf F) . (a,(0. F)) = a ) by Th15, REALSET2:2;
hence  ( a + b = c iff (osf F) . (c,b) = a ) by Th13; ::_thesis: verum
end;

theorem :: REALSET3:18
for F being Field
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; ::_thesis: 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)
let a, b, c be Element of F; ::_thesis: (osf F) . (a,((osf F) . (b,c))) = the addF of F . (((osf F) . (a,b)),c)
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 ; ::_thesis: verum
end;

theorem :: REALSET3:19
for F being Field
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; ::_thesis: 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)
let a, b, c be Element of F; ::_thesis: (osf F) . (a,( the addF of F . (b,c))) = (osf F) . (((osf F) . (a,b)),c)
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 ; ::_thesis: verum
end;

definition
let F be Field;
func ovf F ->  Function of [: the carrier of F,(NonZero F):], the carrier of F means :Def2: :: REALSET3:def 2
 for x being Element of F
for y being Element of NonZero F holds it . (x,y) = (omf F) . (x,((revf F) . y));
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))
proof
defpred S1[ Element of F, Element of NonZero F, set ] means $3 = (omf F) . ($1,((revf F) . $2));
now__::_thesis:_for_x_being_Element_of_F
for_y_being_Element_of_NonZero_F_ex_z_being_Element_of_F_st_z_=_(omf_F)_._(x,((revf_F)_._y))
let x be Element of F; ::_thesis: for y being Element of NonZero F ex z being Element of F st z = (omf F) . (x,((revf F) . y))
let y be Element of NonZero F; ::_thesis: ex z being Element of F st z = (omf F) . (x,((revf F) . y))
 (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 = z; ::_thesis: z = (omf F) . (x,((revf F) . y))
thus  z = (omf F) . (x,((revf F) . y)) ; ::_thesis: verum
end;
then A1: for x being Element of F
for y being Element of NonZero F ex z being Element of F st S1[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
for y being Element of NonZero F holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1);
hence  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)) ; ::_thesis: verum
end;
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
proof
let S1, S2 be Function of [: the carrier of F,(NonZero F):], the carrier of F; ::_thesis: ( ( for x being Element of F
for y being Element of NonZero F holds S1 . (x,y) = (omf F) . (x,((revf F) . y)) ) & ( for x being Element of F
for y being Element of NonZero F holds S2 . (x,y) = (omf F) . (x,((revf F) . y)) ) implies S1 = S2 )
assume that
A2: for x being Element of F
for y being Element of NonZero F holds S1 . (x,y) = (omf F) . (x,((revf F) . y)) and
A3: for x being Element of F
for y being Element of NonZero F holds S2 . (x,y) = (omf F) . (x,((revf F) . y)) ; ::_thesis: S1 = S2
now__::_thesis:_for_p_being_set_st_p_in_[:_the_carrier_of_F,(NonZero_F):]_holds_
S1_._p_=_S2_._p
let p be set ; ::_thesis: ( p in [: the carrier of F,(NonZero F):] implies S1 . p = S2 . p )
assume  p in [: the carrier of F,(NonZero F):] ; ::_thesis: S1 . p = S2 . p
then consider x, y being set  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; ::_thesis: verum
end;
hence  S1 = S2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines ovf REALSET3:def_2_:_
 for F being Field
for b2 being Function of [: the carrier of F,(NonZero F):], the carrier of F holds
( b2 = ovf F iff for x being Element of F
for y being Element of NonZero F holds b2 . (x,y) = (omf F) . (x,((revf F) . y)) );

theorem Th20: :: REALSET3:20
for F being Field
for x being Element of NonZero F holds (ovf F) . (x,x) = 1. F
proof
let F be Field; ::_thesis: for x being Element of NonZero F holds (ovf F) . (x,x) = 1. F
let x be Element of NonZero F; ::_thesis: (ovf F) . (x,x) = 1. F
thus (ovf F) . (x,x) = (omf F) . (x,((revf F) . x)) by Def2
.= 1. F by REALSET2:def_6 ; ::_thesis: verum
end;

theorem Th21: :: REALSET3:21
for F being Field
for a, b being Element of F
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; ::_thesis: for a, b being Element of F
for c being Element of NonZero F holds (omf F) . (a,((ovf F) . (b,c))) = (ovf F) . (((omf F) . (a,b)),c)
let a, b be Element of F; ::_thesis: for c being Element of NonZero F holds (omf F) . (a,((ovf F) . (b,c))) = (ovf F) . (((omf F) . (a,b)),c)
let c be Element of NonZero F; ::_thesis: (omf F) . (a,((ovf F) . (b,c))) = (ovf F) . (((omf F) . (a,b)),c)
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 ; ::_thesis: verum
end;

theorem :: REALSET3:22
for F being Field
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; ::_thesis: 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 )
let a be Element of NonZero F; ::_thesis: ( (omf F) . (a,((ovf F) . ((1. F),a))) = 1. F & (omf F) . (((ovf F) . ((1. F),a)),a) = 1. 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 ; ::_thesis: (omf F) . (((ovf F) . ((1. F),a)),a) = 1. F
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 ; ::_thesis: verum
end;

theorem :: REALSET3:23
for F being Field
for a, b being Element of NonZero F holds (ovf F) . (a,b) = (revf F) . ((ovf F) . (b,a))
proof
let F be Field; ::_thesis: for a, b being Element of NonZero F holds (ovf F) . (a,b) = (revf F) . ((ovf F) . (b,a))
let a, b be Element of NonZero F; ::_thesis: (ovf F) . (a,b) = (revf F) . ((ovf F) . (b,a))
(ovf F) . (a,b) = (omf F) . (a,((revf F) . b)) by Def2
.= (revf F) . ((omf F) . (b,((revf F) . a))) by Th2 ;
hence  (ovf F) . (a,b) = (revf F) . ((ovf F) . (b,a)) by Def2; ::_thesis: verum
end;

theorem :: REALSET3:24
for F being Field
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; ::_thesis: for a, b being Element of NonZero F holds (ovf F) . (((revf F) . a),b) = (revf F) . ((omf F) . (a,b))
let a, b be Element of NonZero F; ::_thesis: (ovf F) . (((revf F) . a),b) = (revf F) . ((omf F) . (a,b))
 (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 ;
::_thesis: verum
end;

theorem Th25: :: REALSET3:25
for F being Field
for a, c being Element of F
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; ::_thesis: for a, c being Element of F
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) )
let a, c be Element of F; ::_thesis: 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) )
let b, d be Element of NonZero F; ::_thesis: ( (ovf F) . (a,b) = (ovf F) . (c,d) iff (omf F) . (a,d) = (omf F) . (b,c) )
 ( (ovf F) . (a,b) = (omf F) . (a,((revf F) . b)) & (ovf F) . (c,d) = (omf F) . (c,((revf F) . d)) ) by Def2;
hence  ( (ovf F) . (a,b) = (ovf F) . (c,d) iff (omf F) . (a,d) = (omf F) . (b,c) ) by Th5; ::_thesis: verum
end;

theorem :: REALSET3:26
for F being Field
for a being Element of NonZero F holds (ovf F) . ((1. F),a) = (revf F) . a
proof
let F be Field; ::_thesis: for a being Element of NonZero F holds (ovf F) . ((1. F),a) = (revf F) . a
let a be Element of NonZero F; ::_thesis: (ovf F) . ((1. F),a) = (revf F) . a
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 ; ::_thesis: verum
end;

theorem Th27: :: REALSET3:27
for F being Field
for a being Element of F holds (ovf F) . (a,(1. F)) = a
proof
let F be Field; ::_thesis: for a being Element of F holds (ovf F) . (a,(1. F)) = a
let a be Element of F; ::_thesis: (ovf F) . (a,(1. F)) = a
 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 ;
::_thesis: verum
end;

theorem :: REALSET3:28
for F being Field
for a being Element of NonZero F
for b, c being Element of F holds
( (omf F) . (a,b) = c iff (ovf F) . (c,a) = b )
proof
let F be Field; ::_thesis: for a being Element of NonZero F
for b, c being Element of F holds
( (omf F) . (a,b) = c iff (ovf F) . (c,a) = b )
let a be Element of NonZero F; ::_thesis: for b, c being Element of F holds
( (omf F) . (a,b) = c iff (ovf F) . (c,a) = b )
let b, c be Element of F; ::_thesis: ( (omf F) . (a,b) = c iff (ovf F) . (c,a) = b )
set d = 1. F;
A1: (omf F) . (c,(1. F)) = c * (1. F)
.= c by REALSET2:21 ;
 ( 1. F is Element of NonZero F & (ovf F) . (b,(1. F)) = b ) by Th27, STRUCT_0:2;
hence  ( (omf F) . (a,b) = c iff (ovf F) . (c,a) = b ) by A1, Th25; ::_thesis: verum
end;

theorem :: REALSET3:29
for F being Field
for a, c being Element of F
for b being Element of NonZero F holds
( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )
proof
let F be Field; ::_thesis: for a, c being Element of F
for b being Element of NonZero F holds
( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )
let a, c be Element of F; ::_thesis: for b being Element of NonZero F holds
( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )
let b be Element of NonZero F; ::_thesis: ( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a )
set d = 1. F;
A1: (omf F) . (c,(1. F)) = c * (1. F)
.= c by REALSET2:21 ;
A2: (omf F) . (b,a) = b * a
.= a * b
.= (omf F) . (a,b) ;
 ( (ovf F) . (a,(1. F)) = a & 1. F is Element of NonZero F ) by Th27, STRUCT_0:2;
hence  ( (omf F) . (a,b) = c iff (ovf F) . (c,b) = a ) by A1, A2, Th25; ::_thesis: verum
end;

theorem :: REALSET3:30
for F being Field
for a being Element of F
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; ::_thesis: for a being Element of F
for b, c being Element of NonZero F holds (ovf F) . (a,((ovf F) . (b,c))) = (omf F) . (((ovf F) . (a,b)),c)
let a be Element of F; ::_thesis: for b, c being Element of NonZero F holds (ovf F) . (a,((ovf F) . (b,c))) = (omf F) . (((ovf F) . (a,b)),c)
let b, c be Element of NonZero F; ::_thesis: (ovf F) . (a,((ovf F) . (b,c))) = (omf F) . (((ovf F) . (a,b)),c)
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 ; ::_thesis: verum
end;

theorem :: REALSET3:31
for F being Field
for a being Element of F
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; ::_thesis: for a being Element of F
for b, c being Element of NonZero F holds (ovf F) . (a,((omf F) . (b,c))) = (ovf F) . (((ovf F) . (a,b)),c)
let a be Element of F; ::_thesis: for b, c being Element of NonZero F holds (ovf F) . (a,((omf F) . (b,c))) = (ovf F) . (((ovf F) . (a,b)),c)
let b, c be Element of NonZero F; ::_thesis: (ovf F) . (a,((omf F) . (b,c))) = (ovf F) . (((ovf F) . (a,b)),c)
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 ;
::_thesis: verum
end;