deffunc H_{1}( Real, Real) -> Element of REAL = In ((max ((sgn $1),(sgn $2))),REAL);

consider f being BinOp of REAL such that

A1: for x, y being Element of REAL holds f . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

A2: for x, y being Element of REAL holds f . (x,y) = max ((sgn x),(sgn y))

the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds

the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds

the Tran of M . [ the InitS of M,[x,y]] = - 1 ) implies for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M )

assume that

A3: M is calculating_type and

A4: the carrier of M = succ REAL and

A5: the FinalS of M = REAL and

A6: the InitS of M = REAL and

A7: the OFun of M = id the carrier of M ; :: thesis: ( ex x, y being Real st

( ( x > 0 or y > 0 ) & not the Tran of M . [ the InitS of M,[x,y]] = 1 ) or ex x, y being Real st

( ( x = 0 or y = 0 ) & x <= 0 & y <= 0 & not the Tran of M . [ the InitS of M,[x,y]] = 0 ) or ex x, y being Real st

( x < 0 & y < 0 & not the Tran of M . [ the InitS of M,[x,y]] = - 1 ) or for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M )

assume that

A8: for x, y being Real st ( x > 0 or y > 0 ) holds

the Tran of M . [ the InitS of M,[x,y]] = 1 and

A9: for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds

the Tran of M . [ the InitS of M,[x,y]] = 0 and

A10: for x, y being Real st x < 0 & y < 0 holds

the Tran of M . [ the InitS of M,[x,y]] = - 1 ; :: thesis: for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M

let x, y be Element of REAL ; :: thesis: max ((sgn x),(sgn y)) is_result_of [x,y],M

hence max ((sgn x),(sgn y)) is_result_of [x,y],M by A2; :: thesis: verum

consider f being BinOp of REAL such that

A1: for x, y being Element of REAL holds f . (x,y) = H

A2: for x, y being Element of REAL holds f . (x,y) = max ((sgn x),(sgn y))

proof

let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; :: thesis: ( M is calculating_type & the carrier of M = succ REAL & the FinalS of M = REAL & the InitS of M = REAL & the OFun of M = id the carrier of M & ( for x, y being Real st ( x > 0 or y > 0 ) holds
let x, y be Element of REAL ; :: thesis: f . (x,y) = max ((sgn x),(sgn y))

reconsider x = x, y = y as Real ;

f . (x,y) = H_{1}(x,y)
by A1;

hence f . (x,y) = max ((sgn x),(sgn y)) ; :: thesis: verum

end;reconsider x = x, y = y as Real ;

f . (x,y) = H

hence f . (x,y) = max ((sgn x),(sgn y)) ; :: thesis: verum

the Tran of M . [ the InitS of M,[x,y]] = 1 ) & ( for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds

the Tran of M . [ the InitS of M,[x,y]] = 0 ) & ( for x, y being Real st x < 0 & y < 0 holds

the Tran of M . [ the InitS of M,[x,y]] = - 1 ) implies for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M )

assume that

A3: M is calculating_type and

A4: the carrier of M = succ REAL and

A5: the FinalS of M = REAL and

A6: the InitS of M = REAL and

A7: the OFun of M = id the carrier of M ; :: thesis: ( ex x, y being Real st

( ( x > 0 or y > 0 ) & not the Tran of M . [ the InitS of M,[x,y]] = 1 ) or ex x, y being Real st

( ( x = 0 or y = 0 ) & x <= 0 & y <= 0 & not the Tran of M . [ the InitS of M,[x,y]] = 0 ) or ex x, y being Real st

( x < 0 & y < 0 & not the Tran of M . [ the InitS of M,[x,y]] = - 1 ) or for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M )

assume that

A8: for x, y being Real st ( x > 0 or y > 0 ) holds

the Tran of M . [ the InitS of M,[x,y]] = 1 and

A9: for x, y being Real st ( x = 0 or y = 0 ) & x <= 0 & y <= 0 holds

the Tran of M . [ the InitS of M,[x,y]] = 0 and

A10: for x, y being Real st x < 0 & y < 0 holds

the Tran of M . [ the InitS of M,[x,y]] = - 1 ; :: thesis: for x, y being Element of REAL holds max ((sgn x),(sgn y)) is_result_of [x,y],M

let x, y be Element of REAL ; :: thesis: max ((sgn x),(sgn y)) is_result_of [x,y],M

now :: thesis: for x, y being Element of REAL holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)

then
f . (x,y) is_result_of [x,y],M
by A3, A4, A5, A6, A7, Th22;let x, y be Element of REAL ; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)

the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)

end;the Tran of M . [ the InitS of M,[x,y]] = H

proof
_{1}(x,y)
; :: thesis: verum

end;

hence
the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)
by A2; :: thesis: verumnow :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)end;

hence
the Tran of M . [ the InitS of M,[x,y]] = Hper cases
( x > 0 or x = 0 or x < 0 )
;

end;

suppose A11:
x > 0
; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)

then A12:
sgn x = 1
by ABSVALUE:def 2;

_{1}(x,y)
; :: thesis: verum

end;now :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)end;

hence
the Tran of M . [ the InitS of M,[x,y]] = Hper cases
( y > 0 or y = 0 or y < 0 )
;

end;

suppose
y > 0
; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)

then
sgn y = 1
by ABSVALUE:def 2;

hence the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)
by A8, A11, A12; :: thesis: verum

end;hence the Tran of M . [ the InitS of M,[x,y]] = H

suppose A13:
x = 0
; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)

then A14:
sgn x = 0
by ABSVALUE:def 2;

_{1}(x,y)
; :: thesis: verum

end;now :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)end;

hence
the Tran of M . [ the InitS of M,[x,y]] = Hper cases
( y > 0 or y = 0 or y < 0 )
;

end;

suppose A15:
y > 0
; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)

then
sgn y = 1
by ABSVALUE:def 2;

then max ((sgn x),(sgn y)) = 1 by A14, XXREAL_0:def 10;

hence the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)
by A8, A15; :: thesis: verum

end;then max ((sgn x),(sgn y)) = 1 by A14, XXREAL_0:def 10;

hence the Tran of M . [ the InitS of M,[x,y]] = H

suppose A18:
x < 0
; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)

then A19:
sgn x = - 1
by ABSVALUE:def 2;

_{1}(x,y)
; :: thesis: verum

end;now :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)end;

hence
the Tran of M . [ the InitS of M,[x,y]] = Hper cases
( y > 0 or y = 0 or y < 0 )
;

end;

suppose A20:
y > 0
; :: thesis: the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)

then
sgn y = 1
by ABSVALUE:def 2;

then max ((sgn x),(sgn y)) = 1 by A19, XXREAL_0:def 10;

hence the Tran of M . [ the InitS of M,[x,y]] = H_{1}(x,y)
by A8, A20; :: thesis: verum

end;then max ((sgn x),(sgn y)) = 1 by A19, XXREAL_0:def 10;

hence the Tran of M . [ the InitS of M,[x,y]] = H

hence max ((sgn x),(sgn y)) is_result_of [x,y],M by A2; :: thesis: verum