:: BINOP_2 semantic presentation

begin

scheme :: BINOP_2:sch 1
FuncDefUniq{ F1() ->  non empty set , F2() ->  non empty set , F3( Element of F1()) ->  set } :
 for f1, f2 being Function of F1(),F2() st ( for x being Element of F1() holds f1 . x = F3(x) ) & ( for x being Element of F1() holds f2 . x = F3(x) ) holds
f1 = f2
proof
let f1, f2 be Function of F1(),F2(); ::_thesis: ( ( for x being Element of F1() holds f1 . x = F3(x) ) & ( for x being Element of F1() holds f2 . x = F3(x) ) implies f1 = f2 )
assume that
A1: for x being Element of F1() holds f1 . x = F3(x) and
A2: for x being Element of F1() holds f2 . x = F3(x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_F1()_holds_f1_._x_=_f2_._x
let x be Element of F1(); ::_thesis: f1 . x = f2 . x
thus f1 . x = F3(x) by A1
.= f2 . x by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

scheme :: BINOP_2:sch 2
BinOpDefuniq{ F1() ->  non empty set , F2( Element of F1(), Element of F1()) ->  set } :
 for o1, o2 being BinOp of F1() st ( for a, b being Element of F1() holds o1 . (a,b) = F2(a,b) ) & ( for a, b being Element of F1() holds o2 . (a,b) = F2(a,b) ) holds
o1 = o2
proof
let o1, o2 be BinOp of F1(); ::_thesis: ( ( for a, b being Element of F1() holds o1 . (a,b) = F2(a,b) ) & ( for a, b being Element of F1() holds o2 . (a,b) = F2(a,b) ) implies o1 = o2 )
assume that
A1: for a, b being Element of F1() holds o1 . (a,b) = F2(a,b) and
A2: for a, b being Element of F1() holds o2 . (a,b) = F2(a,b) ; ::_thesis: o1 = o2
now__::_thesis:_for_a,_b_being_Element_of_F1()_holds_o1_._(a,b)_=_o2_._(a,b)
let a, b be Element of F1(); ::_thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = F2(a,b) by A1
.= o2 . (a,b) by A2 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;

scheme :: BINOP_2:sch 3
CFuncDefUniq{ F1( complex number ) ->  set } :
 for f1, f2 being Function of COMPLEX,COMPLEX st ( for x being complex number holds f1 . x = F1(x) ) & ( for x being complex number holds f2 . x = F1(x) ) holds
f1 = f2
proof
let f1, f2 be Function of COMPLEX,COMPLEX; ::_thesis: ( ( for x being complex number holds f1 . x = F1(x) ) & ( for x being complex number holds f2 . x = F1(x) ) implies f1 = f2 )
assume that
A1: for x being complex number holds f1 . x = F1(x) and
A2: for x being complex number holds f2 . x = F1(x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_COMPLEX_holds_f1_._x_=_f2_._x
let x be Element of COMPLEX ; ::_thesis: f1 . x = f2 . x
thus f1 . x = F1(x) by A1
.= f2 . x by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

scheme :: BINOP_2:sch 4
RFuncDefUniq{ F1( real number ) ->  set } :
 for f1, f2 being Function of REAL,REAL st ( for x being real number holds f1 . x = F1(x) ) & ( for x being real number holds f2 . x = F1(x) ) holds
f1 = f2
proof
let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for x being real number holds f1 . x = F1(x) ) & ( for x being real number holds f2 . x = F1(x) ) implies f1 = f2 )
assume that
A1: for x being real number holds f1 . x = F1(x) and
A2: for x being real number holds f2 . x = F1(x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_REAL_holds_f1_._x_=_f2_._x
let x be Element of REAL ; ::_thesis: f1 . x = f2 . x
thus f1 . x = F1(x) by A1
.= f2 . x by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

registration
cluster  ->  rational for Element of RAT ;
coherence
 for b1 being Element of RAT holds b1 is rational by RAT_1:def_2;
end;

scheme :: BINOP_2:sch 5
WFuncDefUniq{ F1( rational number ) ->  set } :
 for f1, f2 being Function of RAT,RAT st ( for x being rational number holds f1 . x = F1(x) ) & ( for x being rational number holds f2 . x = F1(x) ) holds
f1 = f2
proof
let f1, f2 be Function of RAT,RAT; ::_thesis: ( ( for x being rational number holds f1 . x = F1(x) ) & ( for x being rational number holds f2 . x = F1(x) ) implies f1 = f2 )
assume that
A1: for x being rational number holds f1 . x = F1(x) and
A2: for x being rational number holds f2 . x = F1(x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_RAT_holds_f1_._x_=_f2_._x
let x be Element of RAT ; ::_thesis: f1 . x = f2 . x
thus f1 . x = F1(x) by A1
.= f2 . x by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

scheme :: BINOP_2:sch 6
IFuncDefUniq{ F1( integer number ) ->  set } :
 for f1, f2 being Function of INT,INT st ( for x being integer number holds f1 . x = F1(x) ) & ( for x being integer number holds f2 . x = F1(x) ) holds
f1 = f2
proof
let f1, f2 be Function of INT,INT; ::_thesis: ( ( for x being integer number holds f1 . x = F1(x) ) & ( for x being integer number holds f2 . x = F1(x) ) implies f1 = f2 )
assume that
A1: for x being integer number holds f1 . x = F1(x) and
A2: for x being integer number holds f2 . x = F1(x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_INT_holds_f1_._x_=_f2_._x
let x be Element of INT ; ::_thesis: f1 . x = f2 . x
thus f1 . x = F1(x) by A1
.= f2 . x by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

scheme :: BINOP_2:sch 7
NFuncDefUniq{ F1( Nat) ->  set } :
 for f1, f2 being Function of NAT,NAT st ( for x being Nat holds f1 . x = F1(x) ) & ( for x being Nat holds f2 . x = F1(x) ) holds
f1 = f2
proof
let f1, f2 be Function of NAT,NAT; ::_thesis: ( ( for x being Nat holds f1 . x = F1(x) ) & ( for x being Nat holds f2 . x = F1(x) ) implies f1 = f2 )
assume that
A1: for x being Nat holds f1 . x = F1(x) and
A2: for x being Nat holds f2 . x = F1(x) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_NAT_holds_f1_._x_=_f2_._x
let x be Element of NAT ; ::_thesis: f1 . x = f2 . x
thus f1 . x = F1(x) by A1
.= f2 . x by A2 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;

scheme :: BINOP_2:sch 8
CBinOpDefuniq{ F1( complex number , complex number ) ->  set } :
 for o1, o2 being BinOp of COMPLEX st ( for a, b being complex number holds o1 . (a,b) = F1(a,b) ) & ( for a, b being complex number holds o2 . (a,b) = F1(a,b) ) holds
o1 = o2
proof
let o1, o2 be BinOp of COMPLEX; ::_thesis: ( ( for a, b being complex number holds o1 . (a,b) = F1(a,b) ) & ( for a, b being complex number holds o2 . (a,b) = F1(a,b) ) implies o1 = o2 )
assume that
A1: for a, b being complex number holds o1 . (a,b) = F1(a,b) and
A2: for a, b being complex number holds o2 . (a,b) = F1(a,b) ; ::_thesis: o1 = o2
now__::_thesis:_for_a,_b_being_Element_of_COMPLEX_holds_o1_._(a,b)_=_o2_._(a,b)
let a, b be Element of COMPLEX ; ::_thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = F1(a,b) by A1
.= o2 . (a,b) by A2 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;

scheme :: BINOP_2:sch 9
RBinOpDefuniq{ F1( real number , real number ) ->  set } :
 for o1, o2 being BinOp of REAL st ( for a, b being real number holds o1 . (a,b) = F1(a,b) ) & ( for a, b being real number holds o2 . (a,b) = F1(a,b) ) holds
o1 = o2
proof
let o1, o2 be BinOp of REAL; ::_thesis: ( ( for a, b being real number holds o1 . (a,b) = F1(a,b) ) & ( for a, b being real number holds o2 . (a,b) = F1(a,b) ) implies o1 = o2 )
assume that
A1: for a, b being real number holds o1 . (a,b) = F1(a,b) and
A2: for a, b being real number holds o2 . (a,b) = F1(a,b) ; ::_thesis: o1 = o2
now__::_thesis:_for_a,_b_being_Element_of_REAL_holds_o1_._(a,b)_=_o2_._(a,b)
let a, b be Element of REAL ; ::_thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = F1(a,b) by A1
.= o2 . (a,b) by A2 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;

scheme :: BINOP_2:sch 10
WBinOpDefuniq{ F1( rational number , rational number ) ->  set } :
 for o1, o2 being BinOp of RAT st ( for a, b being rational number holds o1 . (a,b) = F1(a,b) ) & ( for a, b being rational number holds o2 . (a,b) = F1(a,b) ) holds
o1 = o2
proof
let o1, o2 be BinOp of RAT; ::_thesis: ( ( for a, b being rational number holds o1 . (a,b) = F1(a,b) ) & ( for a, b being rational number holds o2 . (a,b) = F1(a,b) ) implies o1 = o2 )
assume that
A1: for a, b being rational number holds o1 . (a,b) = F1(a,b) and
A2: for a, b being rational number holds o2 . (a,b) = F1(a,b) ; ::_thesis: o1 = o2
now__::_thesis:_for_a,_b_being_Element_of_RAT_holds_o1_._(a,b)_=_o2_._(a,b)
let a, b be Element of RAT ; ::_thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = F1(a,b) by A1
.= o2 . (a,b) by A2 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;

scheme :: BINOP_2:sch 11
IBinOpDefuniq{ F1( integer number , integer number ) ->  set } :
 for o1, o2 being BinOp of INT st ( for a, b being integer number holds o1 . (a,b) = F1(a,b) ) & ( for a, b being integer number holds o2 . (a,b) = F1(a,b) ) holds
o1 = o2
proof
let o1, o2 be BinOp of INT; ::_thesis: ( ( for a, b being integer number holds o1 . (a,b) = F1(a,b) ) & ( for a, b being integer number holds o2 . (a,b) = F1(a,b) ) implies o1 = o2 )
assume that
A1: for a, b being integer number holds o1 . (a,b) = F1(a,b) and
A2: for a, b being integer number holds o2 . (a,b) = F1(a,b) ; ::_thesis: o1 = o2
now__::_thesis:_for_a,_b_being_Element_of_INT_holds_o1_._(a,b)_=_o2_._(a,b)
let a, b be Element of INT ; ::_thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = F1(a,b) by A1
.= o2 . (a,b) by A2 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;

scheme :: BINOP_2:sch 12
NBinOpDefuniq{ F1( Nat, Nat) ->  set } :
 for o1, o2 being BinOp of NAT st ( for a, b being Nat holds o1 . (a,b) = F1(a,b) ) & ( for a, b being Nat holds o2 . (a,b) = F1(a,b) ) holds
o1 = o2
proof
let o1, o2 be BinOp of NAT; ::_thesis: ( ( for a, b being Nat holds o1 . (a,b) = F1(a,b) ) & ( for a, b being Nat holds o2 . (a,b) = F1(a,b) ) implies o1 = o2 )
assume that
A1: for a, b being Nat holds o1 . (a,b) = F1(a,b) and
A2: for a, b being Nat holds o2 . (a,b) = F1(a,b) ; ::_thesis: o1 = o2
now__::_thesis:_for_a,_b_being_Element_of_NAT_holds_o1_._(a,b)_=_o2_._(a,b)
let a, b be Element of NAT ; ::_thesis: o1 . (a,b) = o2 . (a,b)
thus o1 . (a,b) = F1(a,b) by A1
.= o2 . (a,b) by A2 ; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;

scheme :: BINOP_2:sch 13
CLambda2D{ F1( complex number , complex number ) ->  complex number } :
 ex f being Function of [:COMPLEX,COMPLEX:],COMPLEX st
for x, y being complex number holds f . (x,y) = F1(x,y)
proof
defpred S1[ complex number , complex number , set ] means $3 = F1($1,$2);
A1: for x, y being Element of COMPLEX ex z being Element of COMPLEX st S1[x,y,z]
proof
let x, y be Element of COMPLEX ; ::_thesis: ex z being Element of COMPLEX st S1[x,y,z]
reconsider z = F1(x,y) as Element of COMPLEX by XCMPLX_0:def_2;
take  z ; ::_thesis: S1[x,y,z]
thus  S1[x,y,z] ; ::_thesis: verum
end;
consider f being Function of [:COMPLEX,COMPLEX:],COMPLEX such that
A2: for x, y being Element of COMPLEX holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1);
take  f ; ::_thesis: for x, y being complex number holds f . (x,y) = F1(x,y)
let x, y be complex number ; ::_thesis: f . (x,y) = F1(x,y)
reconsider x = x, y = y as Element of COMPLEX by XCMPLX_0:def_2;
 S1[x,y,f . (x,y)] by A2;
then  f . (x,y) = F1(x,y) ;
hence  f . (x,y) = F1(x,y) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 14
RLambda2D{ F1( real number , real number ) ->  real number } :
 ex f being Function of [:REAL,REAL:],REAL st
for x, y being real number holds f . (x,y) = F1(x,y)
proof
defpred S1[ real number , real number , set ] means $3 = F1($1,$2);
A1: for x, y being Element of REAL ex z being Element of REAL st S1[x,y,z]
proof
let x, y be Element of REAL ; ::_thesis: ex z being Element of REAL st S1[x,y,z]
reconsider z = F1(x,y) as Element of REAL by XREAL_0:def_1;
take  z ; ::_thesis: S1[x,y,z]
thus  S1[x,y,z] ; ::_thesis: verum
end;
consider f being Function of [:REAL,REAL:],REAL such that
A2: for x, y being Element of REAL holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1);
take  f ; ::_thesis: for x, y being real number holds f . (x,y) = F1(x,y)
let x, y be real number ; ::_thesis: f . (x,y) = F1(x,y)
reconsider x = x, y = y as Element of REAL by XREAL_0:def_1;
 S1[x,y,f . (x,y)] by A2;
then  f . (x,y) = F1(x,y) ;
hence  f . (x,y) = F1(x,y) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 15
WLambda2D{ F1( rational number , rational number ) ->  rational number } :
 ex f being Function of [:RAT,RAT:],RAT st
for x, y being rational number holds f . (x,y) = F1(x,y)
proof
defpred S1[ rational number , rational number , set ] means $3 = F1($1,$2);
A1: for x, y being Element of RAT ex z being Element of RAT st S1[x,y,z]
proof
let x, y be Element of RAT ; ::_thesis: ex z being Element of RAT st S1[x,y,z]
reconsider z = F1(x,y) as Element of RAT by RAT_1:def_2;
take  z ; ::_thesis: S1[x,y,z]
thus  S1[x,y,z] ; ::_thesis: verum
end;
consider f being Function of [:RAT,RAT:],RAT such that
A2: for x, y being Element of RAT holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1);
take  f ; ::_thesis: for x, y being rational number holds f . (x,y) = F1(x,y)
let x, y be rational number ; ::_thesis: f . (x,y) = F1(x,y)
reconsider x = x, y = y as Element of RAT by RAT_1:def_2;
 S1[x,y,f . (x,y)] by A2;
then  f . (x,y) = F1(x,y) ;
hence  f . (x,y) = F1(x,y) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 16
ILambda2D{ F1( integer number , integer number ) ->  integer number } :
 ex f being Function of [:INT,INT:],INT st
for x, y being integer number holds f . (x,y) = F1(x,y)
proof
defpred S1[ integer number , integer number , set ] means $3 = F1($1,$2);
A1: for x, y being Element of INT ex z being Element of INT st S1[x,y,z]
proof
let x, y be Element of INT ; ::_thesis: ex z being Element of INT st S1[x,y,z]
reconsider z = F1(x,y) as Element of INT by INT_1:def_2;
take  z ; ::_thesis: S1[x,y,z]
thus  S1[x,y,z] ; ::_thesis: verum
end;
consider f being Function of [:INT,INT:],INT such that
A2: for x, y being Element of INT holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1);
take  f ; ::_thesis: for x, y being integer number holds f . (x,y) = F1(x,y)
let x, y be integer number ; ::_thesis: f . (x,y) = F1(x,y)
reconsider x = x, y = y as Element of INT by INT_1:def_2;
 S1[x,y,f . (x,y)] by A2;
then  f . (x,y) = F1(x,y) ;
hence  f . (x,y) = F1(x,y) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 17
NLambda2D{ F1( Nat, Nat) ->  Nat } :
 ex f being Function of [:NAT,NAT:],NAT st
for x, y being Nat holds f . (x,y) = F1(x,y)
proof
defpred S1[ Nat, Nat, set ] means $3 = F1($1,$2);
A1: for x, y being Element of NAT ex z being Element of NAT st S1[x,y,z]
proof
let x, y be Element of NAT ; ::_thesis: ex z being Element of NAT st S1[x,y,z]
reconsider z = F1(x,y) as Element of NAT by ORDINAL1:def_12;
take  z ; ::_thesis: S1[x,y,z]
thus  S1[x,y,z] ; ::_thesis: verum
end;
consider f being Function of [:NAT,NAT:],NAT such that
A2: for x, y being Element of NAT holds S1[x,y,f . (x,y)] from BINOP_1:sch_3(A1);
take  f ; ::_thesis: for x, y being Nat holds f . (x,y) = F1(x,y)
let x, y be Nat; ::_thesis: f . (x,y) = F1(x,y)
reconsider x = x, y = y as Element of NAT by ORDINAL1:def_12;
 S1[x,y,f . (x,y)] by A2;
then  f . (x,y) = F1(x,y) ;
hence  f . (x,y) = F1(x,y) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 18
CLambdaD{ F1( complex number ) ->  complex number } :
 ex f being Function of COMPLEX,COMPLEX st
for x being complex number holds f . x = F1(x)
proof
defpred S1[ Element of COMPLEX , set ] means $2 = F1($1);
A1: for x being Element of COMPLEX ex y being Element of COMPLEX st S1[x,y]
proof
let x be Element of COMPLEX ; ::_thesis: ex y being Element of COMPLEX st S1[x,y]
reconsider y = F1(x) as Element of COMPLEX by XCMPLX_0:def_2;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function of COMPLEX,COMPLEX such that
A2: for x being Element of COMPLEX holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for x being complex number holds f . x = F1(x)
let c be complex number ; ::_thesis: f . c = F1(c)
reconsider c = c as Element of COMPLEX by XCMPLX_0:def_2;
 S1[c,f . c] by A2;
hence  f . c = F1(c) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 19
RLambdaD{ F1( real number ) ->  real number } :
 ex f being Function of REAL,REAL st
for x being real number holds f . x = F1(x)
proof
defpred S1[ Element of REAL , set ] means $2 = F1($1);
A1: for x being Element of REAL ex y being Element of REAL st S1[x,y]
proof
let x be Element of REAL ; ::_thesis: ex y being Element of REAL st S1[x,y]
reconsider y = F1(x) as Element of REAL by XREAL_0:def_1;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function of REAL,REAL such that
A2: for x being Element of REAL holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for x being real number holds f . x = F1(x)
let c be real number ; ::_thesis: f . c = F1(c)
reconsider c = c as Element of REAL by XREAL_0:def_1;
 S1[c,f . c] by A2;
hence  f . c = F1(c) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 20
WLambdaD{ F1( rational number ) ->  rational number } :
 ex f being Function of RAT,RAT st
for x being rational number holds f . x = F1(x)
proof
defpred S1[ Element of RAT , set ] means $2 = F1($1);
A1: for x being Element of RAT ex y being Element of RAT st S1[x,y]
proof
let x be Element of RAT ; ::_thesis: ex y being Element of RAT st S1[x,y]
reconsider y = F1(x) as Element of RAT by RAT_1:def_2;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function of RAT,RAT such that
A2: for x being Element of RAT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for x being rational number holds f . x = F1(x)
let c be rational number ; ::_thesis: f . c = F1(c)
reconsider c = c as Element of RAT by RAT_1:def_2;
 S1[c,f . c] by A2;
hence  f . c = F1(c) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 21
ILambdaD{ F1( integer number ) ->  integer number } :
 ex f being Function of INT,INT st
for x being integer number holds f . x = F1(x)
proof
defpred S1[ Element of INT , set ] means $2 = F1($1);
A1: for x being Element of INT ex y being Element of INT st S1[x,y]
proof
let x be Element of INT ; ::_thesis: ex y being Element of INT st S1[x,y]
reconsider y = F1(x) as Element of INT by INT_1:def_2;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function of INT,INT such that
A2: for x being Element of INT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for x being integer number holds f . x = F1(x)
let c be integer number ; ::_thesis: f . c = F1(c)
reconsider c = c as Element of INT by INT_1:def_2;
 S1[c,f . c] by A2;
hence  f . c = F1(c) ; ::_thesis: verum
end;

scheme :: BINOP_2:sch 22
NLambdaD{ F1( Nat) ->  Nat } :
 ex f being Function of NAT,NAT st
for x being Nat holds f . x = F1(x)
proof
defpred S1[ Element of NAT , set ] means $2 = F1($1);
A1: for x being Element of NAT ex y being Element of NAT st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of NAT st S1[x,y]
reconsider y = F1(x) as Element of NAT by ORDINAL1:def_12;
take  y ; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function of NAT,NAT such that
A2: for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take  f ; ::_thesis: for x being Nat holds f . x = F1(x)
let c be Nat; ::_thesis: f . c = F1(c)
reconsider c = c as Element of NAT by ORDINAL1:def_12;
 S1[c,f . c] by A2;
hence  f . c = F1(c) ; ::_thesis: verum
end;


definition
let c1 be complex number ;
:: original: -
redefine func - c1 ->  Element of COMPLEX ;
coherence
 - c1 is Element of COMPLEX by XCMPLX_0:def_2;
:: original: "
redefine funcc1 "  ->  Element of COMPLEX ;
coherence
 c1 " is Element of COMPLEX by XCMPLX_0:def_2;
let c2 be complex number ;
:: original: +
redefine funcc1 + c2 ->  Element of COMPLEX ;
coherence
 c1 + c2 is Element of COMPLEX by XCMPLX_0:def_2;
:: original: -
redefine funcc1 - c2 ->  Element of COMPLEX ;
coherence
 c1 - c2 is Element of COMPLEX by XCMPLX_0:def_2;
:: original: *
redefine funcc1 * c2 ->  Element of COMPLEX ;
coherence
 c1 * c2 is Element of COMPLEX by XCMPLX_0:def_2;
:: original: /
redefine funcc1 / c2 ->  Element of COMPLEX ;
coherence
 c1 / c2 is Element of COMPLEX by XCMPLX_0:def_2;
end;


definition
let r1 be real number ;
:: original: -
redefine func - r1 ->  Element of REAL ;
coherence
 - r1 is Element of REAL by XREAL_0:def_1;
:: original: "
redefine funcr1 "  ->  Element of REAL ;
coherence
 r1 " is Element of REAL by XREAL_0:def_1;
let r2 be real number ;
:: original: +
redefine funcr1 + r2 ->  Element of REAL ;
coherence
 r1 + r2 is Element of REAL by XREAL_0:def_1;
:: original: -
redefine funcr1 - r2 ->  Element of REAL ;
coherence
 r1 - r2 is Element of REAL by XREAL_0:def_1;
:: original: *
redefine funcr1 * r2 ->  Element of REAL ;
coherence
 r1 * r2 is Element of REAL by XREAL_0:def_1;
:: original: /
redefine funcr1 / r2 ->  Element of REAL ;
coherence
 r1 / r2 is Element of REAL by XREAL_0:def_1;
end;


definition
let w1 be rational number ;
:: original: -
redefine func - w1 ->  Element of RAT ;
coherence
 - w1 is Element of RAT by RAT_1:def_2;
:: original: "
redefine funcw1 "  ->  Element of RAT ;
coherence
 w1 " is Element of RAT by RAT_1:def_2;
let w2 be rational number ;
:: original: +
redefine funcw1 + w2 ->  Element of RAT ;
coherence
 w1 + w2 is Element of RAT by RAT_1:def_2;
:: original: -
redefine funcw1 - w2 ->  Element of RAT ;
coherence
 w1 - w2 is Element of RAT by RAT_1:def_2;
:: original: *
redefine funcw1 * w2 ->  Element of RAT ;
coherence
 w1 * w2 is Element of RAT by RAT_1:def_2;
:: original: /
redefine funcw1 / w2 ->  Element of RAT ;
coherence
 w1 / w2 is Element of RAT by RAT_1:def_2;
end;


definition
let i1 be integer number ;
:: original: -
redefine func - i1 ->  Element of INT ;
coherence
 - i1 is Element of INT by INT_1:def_2;
let i2 be integer number ;
:: original: +
redefine funci1 + i2 ->  Element of INT ;
coherence
 i1 + i2 is Element of INT by INT_1:def_2;
:: original: -
redefine funci1 - i2 ->  Element of INT ;
coherence
 i1 - i2 is Element of INT by INT_1:def_2;
:: original: *
redefine funci1 * i2 ->  Element of INT ;
coherence
 i1 * i2 is Element of INT by INT_1:def_2;
end;


definition
let n1, n2 be Nat;
:: original: +
redefine funcn1 + n2 ->  Element of NAT ;
coherence
 n1 + n2 is Element of NAT by ORDINAL1:def_12;
:: original: *
redefine funcn1 * n2 ->  Element of NAT ;
coherence
 n1 * n2 is Element of NAT by ORDINAL1:def_12;
end;

definition
func compcomplex  ->  UnOp of COMPLEX means :: BINOP_2:def 1
 for c being complex number holds it . c = - c;
existence
 ex b1 being UnOp of COMPLEX st
for c being complex number holds b1 . c = - c from BINOP_2:sch_18();
uniqueness
 for b1, b2 being UnOp of COMPLEX st ( for c being complex number holds b1 . c = - c ) & ( for c being complex number holds b2 . c = - c ) holds
b1 = b2 from BINOP_2:sch_3();
func invcomplex  ->  UnOp of COMPLEX means :: BINOP_2:def 2
 for c being complex number holds it . c = c " ;
existence
 ex b1 being UnOp of COMPLEX st
for c being complex number holds b1 . c = c " from BINOP_2:sch_18();
uniqueness
 for b1, b2 being UnOp of COMPLEX st ( for c being complex number holds b1 . c = c " ) & ( for c being complex number holds b2 . c = c " ) holds
b1 = b2 from BINOP_2:sch_3();
func addcomplex  ->  BinOp of COMPLEX means :Def3: :: BINOP_2:def 3
 for c1, c2 being complex number holds it . (c1,c2) = c1 + c2;
existence
 ex b1 being BinOp of COMPLEX st
for c1, c2 being complex number holds b1 . (c1,c2) = c1 + c2 from BINOP_2:sch_13();
uniqueness
 for b1, b2 being BinOp of COMPLEX st ( for c1, c2 being complex number holds b1 . (c1,c2) = c1 + c2 ) & ( for c1, c2 being complex number holds b2 . (c1,c2) = c1 + c2 ) holds
b1 = b2 from BINOP_2:sch_8();
func diffcomplex  ->  BinOp of COMPLEX means :: BINOP_2:def 4
 for c1, c2 being complex number holds it . (c1,c2) = c1 - c2;
existence
 ex b1 being BinOp of COMPLEX st
for c1, c2 being complex number holds b1 . (c1,c2) = c1 - c2 from BINOP_2:sch_13();
uniqueness
 for b1, b2 being BinOp of COMPLEX st ( for c1, c2 being complex number holds b1 . (c1,c2) = c1 - c2 ) & ( for c1, c2 being complex number holds b2 . (c1,c2) = c1 - c2 ) holds
b1 = b2 from BINOP_2:sch_8();
func multcomplex  ->  BinOp of COMPLEX means :Def5: :: BINOP_2:def 5
 for c1, c2 being complex number holds it . (c1,c2) = c1 * c2;
existence
 ex b1 being BinOp of COMPLEX st
for c1, c2 being complex number holds b1 . (c1,c2) = c1 * c2 from BINOP_2:sch_13();
uniqueness
 for b1, b2 being BinOp of COMPLEX st ( for c1, c2 being complex number holds b1 . (c1,c2) = c1 * c2 ) & ( for c1, c2 being complex number holds b2 . (c1,c2) = c1 * c2 ) holds
b1 = b2 from BINOP_2:sch_8();
func divcomplex  ->  BinOp of COMPLEX means :: BINOP_2:def 6
 for c1, c2 being complex number holds it . (c1,c2) = c1 / c2;
existence
 ex b1 being BinOp of COMPLEX st
for c1, c2 being complex number holds b1 . (c1,c2) = c1 / c2 from BINOP_2:sch_13();
uniqueness
 for b1, b2 being BinOp of COMPLEX st ( for c1, c2 being complex number holds b1 . (c1,c2) = c1 / c2 ) & ( for c1, c2 being complex number holds b2 . (c1,c2) = c1 / c2 ) holds
b1 = b2 from BINOP_2:sch_8();
end;

:: deftheorem  defines compcomplex BINOP_2:def_1_:_
 for b1 being UnOp of COMPLEX holds
( b1 = compcomplex iff for c being complex number holds b1 . c = - c );

:: deftheorem  defines invcomplex BINOP_2:def_2_:_
 for b1 being UnOp of COMPLEX holds
( b1 = invcomplex iff for c being complex number holds b1 . c = c " );

:: deftheorem Def3 defines addcomplex BINOP_2:def_3_:_
 for b1 being BinOp of COMPLEX holds
( b1 = addcomplex iff for c1, c2 being complex number holds b1 . (c1,c2) = c1 + c2 );

:: deftheorem  defines diffcomplex BINOP_2:def_4_:_
 for b1 being BinOp of COMPLEX holds
( b1 = diffcomplex iff for c1, c2 being complex number holds b1 . (c1,c2) = c1 - c2 );

:: deftheorem Def5 defines multcomplex BINOP_2:def_5_:_
 for b1 being BinOp of COMPLEX holds
( b1 = multcomplex iff for c1, c2 being complex number holds b1 . (c1,c2) = c1 * c2 );

:: deftheorem  defines divcomplex BINOP_2:def_6_:_
 for b1 being BinOp of COMPLEX holds
( b1 = divcomplex iff for c1, c2 being complex number holds b1 . (c1,c2) = c1 / c2 );

definition
func compreal  ->  UnOp of REAL means :: BINOP_2:def 7
 for r being real number holds it . r = - r;
existence
 ex b1 being UnOp of REAL st
for r being real number holds b1 . r = - r from BINOP_2:sch_19();
uniqueness
 for b1, b2 being UnOp of REAL st ( for r being real number holds b1 . r = - r ) & ( for r being real number holds b2 . r = - r ) holds
b1 = b2 from BINOP_2:sch_4();
func invreal  ->  UnOp of REAL means :: BINOP_2:def 8
 for r being real number holds it . r = r " ;
existence
 ex b1 being UnOp of REAL st
for r being real number holds b1 . r = r " from BINOP_2:sch_19();
uniqueness
 for b1, b2 being UnOp of REAL st ( for r being real number holds b1 . r = r " ) & ( for r being real number holds b2 . r = r " ) holds
b1 = b2 from BINOP_2:sch_4();
func addreal  ->  BinOp of REAL means :Def9: :: BINOP_2:def 9
 for r1, r2 being real number holds it . (r1,r2) = r1 + r2;
existence
 ex b1 being BinOp of REAL st
for r1, r2 being real number holds b1 . (r1,r2) = r1 + r2 from BINOP_2:sch_14();
uniqueness
 for b1, b2 being BinOp of REAL st ( for r1, r2 being real number holds b1 . (r1,r2) = r1 + r2 ) & ( for r1, r2 being real number holds b2 . (r1,r2) = r1 + r2 ) holds
b1 = b2 from BINOP_2:sch_9();
func diffreal  ->  BinOp of REAL means :: BINOP_2:def 10
 for r1, r2 being real number holds it . (r1,r2) = r1 - r2;
existence
 ex b1 being BinOp of REAL st
for r1, r2 being real number holds b1 . (r1,r2) = r1 - r2 from BINOP_2:sch_14();
uniqueness
 for b1, b2 being BinOp of REAL st ( for r1, r2 being real number holds b1 . (r1,r2) = r1 - r2 ) & ( for r1, r2 being real number holds b2 . (r1,r2) = r1 - r2 ) holds
b1 = b2 from BINOP_2:sch_9();
func multreal  ->  BinOp of REAL means :Def11: :: BINOP_2:def 11
 for r1, r2 being real number holds it . (r1,r2) = r1 * r2;
existence
 ex b1 being BinOp of REAL st
for r1, r2 being real number holds b1 . (r1,r2) = r1 * r2 from BINOP_2:sch_14();
uniqueness
 for b1, b2 being BinOp of REAL st ( for r1, r2 being real number holds b1 . (r1,r2) = r1 * r2 ) & ( for r1, r2 being real number holds b2 . (r1,r2) = r1 * r2 ) holds
b1 = b2 from BINOP_2:sch_9();
func divreal  ->  BinOp of REAL means :: BINOP_2:def 12
 for r1, r2 being real number holds it . (r1,r2) = r1 / r2;
existence
 ex b1 being BinOp of REAL st
for r1, r2 being real number holds b1 . (r1,r2) = r1 / r2 from BINOP_2:sch_14();
uniqueness
 for b1, b2 being BinOp of REAL st ( for r1, r2 being real number holds b1 . (r1,r2) = r1 / r2 ) & ( for r1, r2 being real number holds b2 . (r1,r2) = r1 / r2 ) holds
b1 = b2 from BINOP_2:sch_9();
end;

:: deftheorem  defines compreal BINOP_2:def_7_:_
 for b1 being UnOp of REAL holds
( b1 = compreal iff for r being real number holds b1 . r = - r );

:: deftheorem  defines invreal BINOP_2:def_8_:_
 for b1 being UnOp of REAL holds
( b1 = invreal iff for r being real number holds b1 . r = r " );

:: deftheorem Def9 defines addreal BINOP_2:def_9_:_
 for b1 being BinOp of REAL holds
( b1 = addreal iff for r1, r2 being real number holds b1 . (r1,r2) = r1 + r2 );

:: deftheorem  defines diffreal BINOP_2:def_10_:_
 for b1 being BinOp of REAL holds
( b1 = diffreal iff for r1, r2 being real number holds b1 . (r1,r2) = r1 - r2 );

:: deftheorem Def11 defines multreal BINOP_2:def_11_:_
 for b1 being BinOp of REAL holds
( b1 = multreal iff for r1, r2 being real number holds b1 . (r1,r2) = r1 * r2 );

:: deftheorem  defines divreal BINOP_2:def_12_:_
 for b1 being BinOp of REAL holds
( b1 = divreal iff for r1, r2 being real number holds b1 . (r1,r2) = r1 / r2 );

definition
func comprat  ->  UnOp of RAT means :: BINOP_2:def 13
 for w being rational number holds it . w = - w;
existence
 ex b1 being UnOp of RAT st
for w being rational number holds b1 . w = - w from BINOP_2:sch_20();
uniqueness
 for b1, b2 being UnOp of RAT st ( for w being rational number holds b1 . w = - w ) & ( for w being rational number holds b2 . w = - w ) holds
b1 = b2 from BINOP_2:sch_5();
func invrat  ->  UnOp of RAT means :: BINOP_2:def 14
 for w being rational number holds it . w = w " ;
existence
 ex b1 being UnOp of RAT st
for w being rational number holds b1 . w = w " from BINOP_2:sch_20();
uniqueness
 for b1, b2 being UnOp of RAT st ( for w being rational number holds b1 . w = w " ) & ( for w being rational number holds b2 . w = w " ) holds
b1 = b2 from BINOP_2:sch_5();
func addrat  ->  BinOp of RAT means :Def15: :: BINOP_2:def 15
 for w1, w2 being rational number holds it . (w1,w2) = w1 + w2;
existence
 ex b1 being BinOp of RAT st
for w1, w2 being rational number holds b1 . (w1,w2) = w1 + w2 from BINOP_2:sch_15();
uniqueness
 for b1, b2 being BinOp of RAT st ( for w1, w2 being rational number holds b1 . (w1,w2) = w1 + w2 ) & ( for w1, w2 being rational number holds b2 . (w1,w2) = w1 + w2 ) holds
b1 = b2 from BINOP_2:sch_10();
func diffrat  ->  BinOp of RAT means :: BINOP_2:def 16
 for w1, w2 being rational number holds it . (w1,w2) = w1 - w2;
existence
 ex b1 being BinOp of RAT st
for w1, w2 being rational number holds b1 . (w1,w2) = w1 - w2 from BINOP_2:sch_15();
uniqueness
 for b1, b2 being BinOp of RAT st ( for w1, w2 being rational number holds b1 . (w1,w2) = w1 - w2 ) & ( for w1, w2 being rational number holds b2 . (w1,w2) = w1 - w2 ) holds
b1 = b2 from BINOP_2:sch_10();
func multrat  ->  BinOp of RAT means :Def17: :: BINOP_2:def 17
 for w1, w2 being rational number holds it . (w1,w2) = w1 * w2;
existence
 ex b1 being BinOp of RAT st
for w1, w2 being rational number holds b1 . (w1,w2) = w1 * w2 from BINOP_2:sch_15();
uniqueness
 for b1, b2 being BinOp of RAT st ( for w1, w2 being rational number holds b1 . (w1,w2) = w1 * w2 ) & ( for w1, w2 being rational number holds b2 . (w1,w2) = w1 * w2 ) holds
b1 = b2 from BINOP_2:sch_10();
func divrat  ->  BinOp of RAT means :: BINOP_2:def 18
 for w1, w2 being rational number holds it . (w1,w2) = w1 / w2;
existence
 ex b1 being BinOp of RAT st
for w1, w2 being rational number holds b1 . (w1,w2) = w1 / w2 from BINOP_2:sch_15();
uniqueness
 for b1, b2 being BinOp of RAT st ( for w1, w2 being rational number holds b1 . (w1,w2) = w1 / w2 ) & ( for w1, w2 being rational number holds b2 . (w1,w2) = w1 / w2 ) holds
b1 = b2 from BINOP_2:sch_10();
end;

:: deftheorem  defines comprat BINOP_2:def_13_:_
 for b1 being UnOp of RAT holds
( b1 = comprat iff for w being rational number holds b1 . w = - w );

:: deftheorem  defines invrat BINOP_2:def_14_:_
 for b1 being UnOp of RAT holds
( b1 = invrat iff for w being rational number holds b1 . w = w " );

:: deftheorem Def15 defines addrat BINOP_2:def_15_:_
 for b1 being BinOp of RAT holds
( b1 = addrat iff for w1, w2 being rational number holds b1 . (w1,w2) = w1 + w2 );

:: deftheorem  defines diffrat BINOP_2:def_16_:_
 for b1 being BinOp of RAT holds
( b1 = diffrat iff for w1, w2 being rational number holds b1 . (w1,w2) = w1 - w2 );

:: deftheorem Def17 defines multrat BINOP_2:def_17_:_
 for b1 being BinOp of RAT holds
( b1 = multrat iff for w1, w2 being rational number holds b1 . (w1,w2) = w1 * w2 );

:: deftheorem  defines divrat BINOP_2:def_18_:_
 for b1 being BinOp of RAT holds
( b1 = divrat iff for w1, w2 being rational number holds b1 . (w1,w2) = w1 / w2 );

definition
func compint  ->  UnOp of INT means :: BINOP_2:def 19
 for i being integer number holds it . i = - i;
existence
 ex b1 being UnOp of INT st
for i being integer number holds b1 . i = - i from BINOP_2:sch_21();
uniqueness
 for b1, b2 being UnOp of INT st ( for i being integer number holds b1 . i = - i ) & ( for i being integer number holds b2 . i = - i ) holds
b1 = b2 from BINOP_2:sch_6();
func addint  ->  BinOp of INT means :Def20: :: BINOP_2:def 20
 for i1, i2 being integer number holds it . (i1,i2) = i1 + i2;
existence
 ex b1 being BinOp of INT st
for i1, i2 being integer number holds b1 . (i1,i2) = i1 + i2 from BINOP_2:sch_16();
uniqueness
 for b1, b2 being BinOp of INT st ( for i1, i2 being integer number holds b1 . (i1,i2) = i1 + i2 ) & ( for i1, i2 being integer number holds b2 . (i1,i2) = i1 + i2 ) holds
b1 = b2 from BINOP_2:sch_11();
func diffint  ->  BinOp of INT means :: BINOP_2:def 21
 for i1, i2 being integer number holds it . (i1,i2) = i1 - i2;
existence
 ex b1 being BinOp of INT st
for i1, i2 being integer number holds b1 . (i1,i2) = i1 - i2 from BINOP_2:sch_16();
uniqueness
 for b1, b2 being BinOp of INT st ( for i1, i2 being integer number holds b1 . (i1,i2) = i1 - i2 ) & ( for i1, i2 being integer number holds b2 . (i1,i2) = i1 - i2 ) holds
b1 = b2 from BINOP_2:sch_11();
func multint  ->  BinOp of INT means :Def22: :: BINOP_2:def 22
 for i1, i2 being integer number holds it . (i1,i2) = i1 * i2;
existence
 ex b1 being BinOp of INT st
for i1, i2 being integer number holds b1 . (i1,i2) = i1 * i2 from BINOP_2:sch_16();
uniqueness
 for b1, b2 being BinOp of INT st ( for i1, i2 being integer number holds b1 . (i1,i2) = i1 * i2 ) & ( for i1, i2 being integer number holds b2 . (i1,i2) = i1 * i2 ) holds
b1 = b2 from BINOP_2:sch_11();
end;

:: deftheorem  defines compint BINOP_2:def_19_:_
 for b1 being UnOp of INT holds
( b1 = compint iff for i being integer number holds b1 . i = - i );

:: deftheorem Def20 defines addint BINOP_2:def_20_:_
 for b1 being BinOp of INT holds
( b1 = addint iff for i1, i2 being integer number holds b1 . (i1,i2) = i1 + i2 );

:: deftheorem  defines diffint BINOP_2:def_21_:_
 for b1 being BinOp of INT holds
( b1 = diffint iff for i1, i2 being integer number holds b1 . (i1,i2) = i1 - i2 );

:: deftheorem Def22 defines multint BINOP_2:def_22_:_
 for b1 being BinOp of INT holds
( b1 = multint iff for i1, i2 being integer number holds b1 . (i1,i2) = i1 * i2 );

definition
func addnat  ->  BinOp of NAT means :Def23: :: BINOP_2:def 23
 for n1, n2 being Nat holds it . (n1,n2) = n1 + n2;
existence
 ex b1 being BinOp of NAT st
for n1, n2 being Nat holds b1 . (n1,n2) = n1 + n2 from BINOP_2:sch_17();
uniqueness
 for b1, b2 being BinOp of NAT st ( for n1, n2 being Nat holds b1 . (n1,n2) = n1 + n2 ) & ( for n1, n2 being Nat holds b2 . (n1,n2) = n1 + n2 ) holds
b1 = b2 from BINOP_2:sch_12();
func multnat  ->  BinOp of NAT means :Def24: :: BINOP_2:def 24
 for n1, n2 being Nat holds it . (n1,n2) = n1 * n2;
existence
 ex b1 being BinOp of NAT st
for n1, n2 being Nat holds b1 . (n1,n2) = n1 * n2 from BINOP_2:sch_17();
uniqueness
 for b1, b2 being BinOp of NAT st ( for n1, n2 being Nat holds b1 . (n1,n2) = n1 * n2 ) & ( for n1, n2 being Nat holds b2 . (n1,n2) = n1 * n2 ) holds
b1 = b2 from BINOP_2:sch_12();
end;

:: deftheorem Def23 defines addnat BINOP_2:def_23_:_
 for b1 being BinOp of NAT holds
( b1 = addnat iff for n1, n2 being Nat holds b1 . (n1,n2) = n1 + n2 );

:: deftheorem Def24 defines multnat BINOP_2:def_24_:_
 for b1 being BinOp of NAT holds
( b1 = multnat iff for n1, n2 being Nat holds b1 . (n1,n2) = n1 * n2 );

registration
cluster addcomplex  ->  commutative associative ;
coherence
 ( addcomplex is commutative & addcomplex is associative )
proof
thus  addcomplex is commutative ::_thesis: addcomplex is associative
proof
let c1, c2 be Element of COMPLEX ; :: according to BINOP_1:def_2 ::_thesis: addcomplex . (c1,c2) = addcomplex . (c2,c1)
thus addcomplex . (c1,c2) = c1 + c2 by Def3
.= addcomplex . (c2,c1) by Def3 ; ::_thesis: verum
end;
let c1, c2, c3 be Element of COMPLEX ; :: according to BINOP_1:def_3 ::_thesis: addcomplex . (c1,(addcomplex . (c2,c3))) = addcomplex . ((addcomplex . (c1,c2)),c3)
thus addcomplex . (c1,(addcomplex . (c2,c3))) = c1 + (addcomplex . (c2,c3)) by Def3
.= c1 + (c2 + c3) by Def3
.= (c1 + c2) + c3
.= (addcomplex . (c1,c2)) + c3 by Def3
.= addcomplex . ((addcomplex . (c1,c2)),c3) by Def3 ; ::_thesis: verum
end;
cluster multcomplex  ->  commutative associative ;
coherence
 ( multcomplex is commutative & multcomplex is associative )
proof
thus  multcomplex is commutative ::_thesis: multcomplex is associative
proof
let c1, c2 be Element of COMPLEX ; :: according to BINOP_1:def_2 ::_thesis: multcomplex . (c1,c2) = multcomplex . (c2,c1)
thus multcomplex . (c1,c2) = c1 * c2 by Def5
.= multcomplex . (c2,c1) by Def5 ; ::_thesis: verum
end;
let c1, c2, c3 be Element of COMPLEX ; :: according to BINOP_1:def_3 ::_thesis: multcomplex . (c1,(multcomplex . (c2,c3))) = multcomplex . ((multcomplex . (c1,c2)),c3)
thus multcomplex . (c1,(multcomplex . (c2,c3))) = c1 * (multcomplex . (c2,c3)) by Def5
.= c1 * (c2 * c3) by Def5
.= (c1 * c2) * c3
.= (multcomplex . (c1,c2)) * c3 by Def5
.= multcomplex . ((multcomplex . (c1,c2)),c3) by Def5 ; ::_thesis: verum
end;
cluster addreal  ->  commutative associative ;
coherence
 ( addreal is commutative & addreal is associative )
proof
thus  addreal is commutative ::_thesis: addreal is associative
proof
let r1, r2 be Element of REAL ; :: according to BINOP_1:def_2 ::_thesis: addreal . (r1,r2) = addreal . (r2,r1)
thus addreal . (r1,r2) = r1 + r2 by Def9
.= addreal . (r2,r1) by Def9 ; ::_thesis: verum
end;
let r1, r2, r3 be Element of REAL ; :: according to BINOP_1:def_3 ::_thesis: addreal . (r1,(addreal . (r2,r3))) = addreal . ((addreal . (r1,r2)),r3)
thus addreal . (r1,(addreal . (r2,r3))) = r1 + (addreal . (r2,r3)) by Def9
.= r1 + (r2 + r3) by Def9
.= (r1 + r2) + r3
.= (addreal . (r1,r2)) + r3 by Def9
.= addreal . ((addreal . (r1,r2)),r3) by Def9 ; ::_thesis: verum
end;
cluster multreal  ->  commutative associative ;
coherence
 ( multreal is commutative & multreal is associative )
proof
thus  multreal is commutative ::_thesis: multreal is associative
proof
let r1, r2 be Element of REAL ; :: according to BINOP_1:def_2 ::_thesis: multreal . (r1,r2) = multreal . (r2,r1)
thus multreal . (r1,r2) = r1 * r2 by Def11
.= multreal . (r2,r1) by Def11 ; ::_thesis: verum
end;
let r1, r2, r3 be Element of REAL ; :: according to BINOP_1:def_3 ::_thesis: multreal . (r1,(multreal . (r2,r3))) = multreal . ((multreal . (r1,r2)),r3)
thus multreal . (r1,(multreal . (r2,r3))) = r1 * (multreal . (r2,r3)) by Def11
.= r1 * (r2 * r3) by Def11
.= (r1 * r2) * r3
.= (multreal . (r1,r2)) * r3 by Def11
.= multreal . ((multreal . (r1,r2)),r3) by Def11 ; ::_thesis: verum
end;
cluster addrat  ->  commutative associative ;
coherence
 ( addrat is commutative & addrat is associative )
proof
thus  addrat is commutative ::_thesis: addrat is associative
proof
let w1, w2 be Element of RAT ; :: according to BINOP_1:def_2 ::_thesis: addrat . (w1,w2) = addrat . (w2,w1)
thus addrat . (w1,w2) = w1 + w2 by Def15
.= addrat . (w2,w1) by Def15 ; ::_thesis: verum
end;
let w1, w2, w3 be Element of RAT ; :: according to BINOP_1:def_3 ::_thesis: addrat . (w1,(addrat . (w2,w3))) = addrat . ((addrat . (w1,w2)),w3)
thus addrat . (w1,(addrat . (w2,w3))) = w1 + (addrat . (w2,w3)) by Def15
.= w1 + (w2 + w3) by Def15
.= (w1 + w2) + w3
.= (addrat . (w1,w2)) + w3 by Def15
.= addrat . ((addrat . (w1,w2)),w3) by Def15 ; ::_thesis: verum
end;
cluster multrat  ->  commutative associative ;
coherence
 ( multrat is commutative & multrat is associative )
proof
thus  multrat is commutative ::_thesis: multrat is associative
proof
let w1, w2 be Element of RAT ; :: according to BINOP_1:def_2 ::_thesis: multrat . (w1,w2) = multrat . (w2,w1)
thus multrat . (w1,w2) = w1 * w2 by Def17
.= multrat . (w2,w1) by Def17 ; ::_thesis: verum
end;
let w1, w2, w3 be Element of RAT ; :: according to BINOP_1:def_3 ::_thesis: multrat . (w1,(multrat . (w2,w3))) = multrat . ((multrat . (w1,w2)),w3)
thus multrat . (w1,(multrat . (w2,w3))) = w1 * (multrat . (w2,w3)) by Def17
.= w1 * (w2 * w3) by Def17
.= (w1 * w2) * w3
.= (multrat . (w1,w2)) * w3 by Def17
.= multrat . ((multrat . (w1,w2)),w3) by Def17 ; ::_thesis: verum
end;
cluster addint  ->  commutative associative ;
coherence
 ( addint is commutative & addint is associative )
proof
thus  addint is commutative ::_thesis: addint is associative
proof
let i1, i2 be Element of INT ; :: according to BINOP_1:def_2 ::_thesis: addint . (i1,i2) = addint . (i2,i1)
thus addint . (i1,i2) = i1 + i2 by Def20
.= addint . (i2,i1) by Def20 ; ::_thesis: verum
end;
let i1, i2, i3 be Element of INT ; :: according to BINOP_1:def_3 ::_thesis: addint . (i1,(addint . (i2,i3))) = addint . ((addint . (i1,i2)),i3)
thus addint . (i1,(addint . (i2,i3))) = i1 + (addint . (i2,i3)) by Def20
.= i1 + (i2 + i3) by Def20
.= (i1 + i2) + i3
.= (addint . (i1,i2)) + i3 by Def20
.= addint . ((addint . (i1,i2)),i3) by Def20 ; ::_thesis: verum
end;
cluster multint  ->  commutative associative ;
coherence
 ( multint is commutative & multint is associative )
proof
thus  multint is commutative ::_thesis: multint is associative
proof
let i1, i2 be Element of INT ; :: according to BINOP_1:def_2 ::_thesis: multint . (i1,i2) = multint . (i2,i1)
thus multint . (i1,i2) = i1 * i2 by Def22
.= multint . (i2,i1) by Def22 ; ::_thesis: verum
end;
let i1, i2, i3 be Element of INT ; :: according to BINOP_1:def_3 ::_thesis: multint . (i1,(multint . (i2,i3))) = multint . ((multint . (i1,i2)),i3)
thus multint . (i1,(multint . (i2,i3))) = i1 * (multint . (i2,i3)) by Def22
.= i1 * (i2 * i3) by Def22
.= (i1 * i2) * i3
.= (multint . (i1,i2)) * i3 by Def22
.= multint . ((multint . (i1,i2)),i3) by Def22 ; ::_thesis: verum
end;
cluster addnat  ->  commutative associative ;
coherence
 ( addnat is commutative & addnat is associative )
proof
thus  addnat is commutative ::_thesis: addnat is associative
proof
let n1, n2 be Element of NAT ; :: according to BINOP_1:def_2 ::_thesis: addnat . (n1,n2) = addnat . (n2,n1)
thus addnat . (n1,n2) = n1 + n2 by Def23
.= addnat . (n2,n1) by Def23 ; ::_thesis: verum
end;
let n1, n2, n3 be Element of NAT ; :: according to BINOP_1:def_3 ::_thesis: addnat . (n1,(addnat . (n2,n3))) = addnat . ((addnat . (n1,n2)),n3)
thus addnat . (n1,(addnat . (n2,n3))) = n1 + (addnat . (n2,n3)) by Def23
.= n1 + (n2 + n3) by Def23
.= (n1 + n2) + n3
.= (addnat . (n1,n2)) + n3 by Def23
.= addnat . ((addnat . (n1,n2)),n3) by Def23 ; ::_thesis: verum
end;
cluster multnat  ->  commutative associative ;
coherence
 ( multnat is commutative & multnat is associative )
proof
thus  multnat is commutative ::_thesis: multnat is associative
proof
let n1, n2 be Element of NAT ; :: according to BINOP_1:def_2 ::_thesis: multnat . (n1,n2) = multnat . (n2,n1)
thus multnat . (n1,n2) = n1 * n2 by Def24
.= multnat . (n2,n1) by Def24 ; ::_thesis: verum
end;
let n1, n2, n3 be Element of NAT ; :: according to BINOP_1:def_3 ::_thesis: multnat . (n1,(multnat . (n2,n3))) = multnat . ((multnat . (n1,n2)),n3)
thus multnat . (n1,(multnat . (n2,n3))) = n1 * (multnat . (n2,n3)) by Def24
.= n1 * (n2 * n3) by Def24
.= (n1 * n2) * n3
.= (multnat . (n1,n2)) * n3 by Def24
.= multnat . ((multnat . (n1,n2)),n3) by Def24 ; ::_thesis: verum
end;
end;

Lm1:  0 in NAT
;

then reconsider z = 0 as Element of COMPLEX by NUMBERS:20;

Lm2:  z is_a_unity_wrt addcomplex
proof
thus  for c being Element of COMPLEX holds addcomplex . (z,c) = c :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: z is_a_right_unity_wrt addcomplex
proof
let c be Element of COMPLEX ; ::_thesis: addcomplex . (z,c) = c
thus addcomplex . (z,c) = 0 + c by Def3
.= c ; ::_thesis: verum
end;
let c be Element of COMPLEX ; :: according to BINOP_1:def_17 ::_thesis: addcomplex . (c,z) = c
thus addcomplex . (c,z) = c + 0 by Def3
.= c ; ::_thesis: verum
end;

Lm3:  0 is_a_unity_wrt addreal
proof
thus  for r being Element of REAL holds addreal . (0,r) = r :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: 0 is_a_right_unity_wrt addreal
proof
let r be Element of REAL ; ::_thesis: addreal . (0,r) = r
thus addreal . (0,r) = 0 + r by Def9
.= r ; ::_thesis: verum
end;
let r be Element of REAL ; :: according to BINOP_1:def_17 ::_thesis: addreal . (r,0) = r
thus addreal . (r,0) = r + 0 by Def9
.= r ; ::_thesis: verum
end;

reconsider z = 0 as Element of RAT by Lm1, NUMBERS:18;

Lm4:  z is_a_unity_wrt addrat
proof
thus  for w being Element of RAT holds addrat . (z,w) = w :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: z is_a_right_unity_wrt addrat
proof
let w be Element of RAT ; ::_thesis: addrat . (z,w) = w
thus addrat . (z,w) = 0 + w by Def15
.= w ; ::_thesis: verum
end;
let w be Element of RAT ; :: according to BINOP_1:def_17 ::_thesis: addrat . (w,z) = w
thus addrat . (w,z) = w + 0 by Def15
.= w ; ::_thesis: verum
end;

reconsider z = 0 as Element of INT by Lm1, NUMBERS:17;

Lm5:  z is_a_unity_wrt addint
proof
thus  for i being Element of INT holds addint . (z,i) = i :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: z is_a_right_unity_wrt addint
proof
let i be Element of INT ; ::_thesis: addint . (z,i) = i
thus addint . (z,i) = 0 + i by Def20
.= i ; ::_thesis: verum
end;
let i be Element of INT ; :: according to BINOP_1:def_17 ::_thesis: addint . (i,z) = i
thus addint . (i,z) = i + 0 by Def20
.= i ; ::_thesis: verum
end;

Lm6:  0 is_a_unity_wrt addnat
proof
thus  for n being Element of NAT holds addnat . (0,n) = n :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: 0 is_a_right_unity_wrt addnat
proof
let n be Element of NAT ; ::_thesis: addnat . (0,n) = n
thus addnat . (0,n) = 0 + n by Def23
.= n ; ::_thesis: verum
end;
let n be Element of NAT ; :: according to BINOP_1:def_17 ::_thesis: addnat . (n,0) = n
thus addnat . (n,0) = n + 0 by Def23
.= n ; ::_thesis: verum
end;

Lm7:  1 in NAT
;

then reconsider z = 1 as Element of COMPLEX by NUMBERS:20;

Lm8:  z is_a_unity_wrt multcomplex
proof
thus  for c being Element of COMPLEX holds multcomplex . (z,c) = c :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: z is_a_right_unity_wrt multcomplex
proof
let c be Element of COMPLEX ; ::_thesis: multcomplex . (z,c) = c
thus multcomplex . (z,c) = 1 * c by Def5
.= c ; ::_thesis: verum
end;
let c be Element of COMPLEX ; :: according to BINOP_1:def_17 ::_thesis: multcomplex . (c,z) = c
thus multcomplex . (c,z) = c * 1 by Def5
.= c ; ::_thesis: verum
end;

Lm9:  1 is_a_unity_wrt multreal
proof
thus  for r being Element of REAL holds multreal . (1,r) = r :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: 1 is_a_right_unity_wrt multreal
proof
let r be Element of REAL ; ::_thesis: multreal . (1,r) = r
thus multreal . (1,r) = 1 * r by Def11
.= r ; ::_thesis: verum
end;
let r be Element of REAL ; :: according to BINOP_1:def_17 ::_thesis: multreal . (r,1) = r
thus multreal . (r,1) = r * 1 by Def11
.= r ; ::_thesis: verum
end;

reconsider z = 1 as Element of RAT by Lm7, NUMBERS:18;

Lm10:  z is_a_unity_wrt multrat
proof
thus  for w being Element of RAT holds multrat . (z,w) = w :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: z is_a_right_unity_wrt multrat
proof
let w be Element of RAT ; ::_thesis: multrat . (z,w) = w
thus multrat . (z,w) = 1 * w by Def17
.= w ; ::_thesis: verum
end;
let w be Element of RAT ; :: according to BINOP_1:def_17 ::_thesis: multrat . (w,z) = w
thus multrat . (w,z) = w * 1 by Def17
.= w ; ::_thesis: verum
end;

reconsider z = 1 as Element of INT by Lm7, NUMBERS:17;

Lm11:  z is_a_unity_wrt multint
proof
thus  for i being Element of INT holds multint . (z,i) = i :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: z is_a_right_unity_wrt multint
proof
let i be Element of INT ; ::_thesis: multint . (z,i) = i
thus multint . (z,i) = 1 * i by Def22
.= i ; ::_thesis: verum
end;
let i be Element of INT ; :: according to BINOP_1:def_17 ::_thesis: multint . (i,z) = i
thus multint . (i,z) = i * 1 by Def22
.= i ; ::_thesis: verum
end;

Lm12:  1 is_a_unity_wrt multnat
proof
thus  for n being Element of NAT holds multnat . (1,n) = n :: according to BINOP_1:def_7,BINOP_1:def_16 ::_thesis: 1 is_a_right_unity_wrt multnat
proof
let n be Element of NAT ; ::_thesis: multnat . (1,n) = n
thus multnat . (1,n) = 1 * n by Def24
.= n ; ::_thesis: verum
end;
let n be Element of NAT ; :: according to BINOP_1:def_17 ::_thesis: multnat . (n,1) = n
thus multnat . (n,1) = n * 1 by Def24
.= n ; ::_thesis: verum
end;

registration
cluster addcomplex  ->  having_a_unity ;
coherence
 addcomplex is having_a_unity by Lm2, SETWISEO:def_2;
cluster addreal  ->  having_a_unity ;
coherence
 addreal is having_a_unity by Lm3, SETWISEO:def_2;
cluster addrat  ->  having_a_unity ;
coherence
 addrat is having_a_unity by Lm4, SETWISEO:def_2;
cluster addint  ->  having_a_unity ;
coherence
 addint is having_a_unity by Lm5, SETWISEO:def_2;
cluster addnat  ->  having_a_unity ;
coherence
 addnat is having_a_unity by Lm6, SETWISEO:def_2;
cluster multcomplex  ->  having_a_unity ;
coherence
 multcomplex is having_a_unity by Lm8, SETWISEO:def_2;
cluster multreal  ->  having_a_unity ;
coherence
 multreal is having_a_unity by Lm9, SETWISEO:def_2;
cluster multrat  ->  having_a_unity ;
coherence
 multrat is having_a_unity by Lm10, SETWISEO:def_2;
cluster multint  ->  having_a_unity ;
coherence
 multint is having_a_unity by Lm11, SETWISEO:def_2;
cluster multnat  ->  having_a_unity ;
coherence
 multnat is having_a_unity by Lm12, SETWISEO:def_2;
end;

theorem :: BINOP_2:1
the_unity_wrt addcomplex = 0 by Lm2, BINOP_1:def_8;

theorem :: BINOP_2:2
the_unity_wrt addreal = 0 by Lm3, BINOP_1:def_8;

theorem :: BINOP_2:3
the_unity_wrt addrat = 0 by Lm4, BINOP_1:def_8;

theorem :: BINOP_2:4
the_unity_wrt addint = 0 by Lm5, BINOP_1:def_8;

theorem :: BINOP_2:5
the_unity_wrt addnat = 0 by Lm6, BINOP_1:def_8;

theorem :: BINOP_2:6
the_unity_wrt multcomplex = 1 by Lm8, BINOP_1:def_8;

theorem :: BINOP_2:7
the_unity_wrt multreal = 1 by Lm9, BINOP_1:def_8;

theorem :: BINOP_2:8
the_unity_wrt multrat = 1 by Lm10, BINOP_1:def_8;

theorem :: BINOP_2:9
the_unity_wrt multint = 1 by Lm11, BINOP_1:def_8;

theorem :: BINOP_2:10
the_unity_wrt multnat = 1 by Lm12, BINOP_1:def_8;