let M be non empty calculating_type halting Moore-SM_Final over [:REAL,REAL:], succ REAL; :: thesis: ( 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

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 Result ([x,y],M) = max ((sgn x),(sgn y)) )

assume that

A1: the carrier of M = succ REAL and

A2: the FinalS of M = REAL and

A3: the InitS of M = REAL and

A4: 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 Result ([x,y],M) = max ((sgn x),(sgn y)) )

assume that

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

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

A6: 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

A7: 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 Result ([x,y],M) = max ((sgn x),(sgn y))

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

max ((sgn x),(sgn y)) in REAL by XREAL_0:def 1;

then A8: max ((sgn x),(sgn y)) in succ REAL by XBOOLE_0:def 3;

max ((sgn x),(sgn y)) is_result_of [x,y],M by A1, A2, A3, A4, A5, A6, A7, Th26;

hence Result ([x,y],M) = max ((sgn x),(sgn y)) by A8, Def9; :: 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 Result ([x,y],M) = max ((sgn x),(sgn y)) )

assume that

A1: the carrier of M = succ REAL and

A2: the FinalS of M = REAL and

A3: the InitS of M = REAL and

A4: 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 Result ([x,y],M) = max ((sgn x),(sgn y)) )

assume that

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

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

A6: 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

A7: 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 Result ([x,y],M) = max ((sgn x),(sgn y))

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

max ((sgn x),(sgn y)) in REAL by XREAL_0:def 1;

then A8: max ((sgn x),(sgn y)) in succ REAL by XBOOLE_0:def 3;

max ((sgn x),(sgn y)) is_result_of [x,y],M by A1, A2, A3, A4, A5, A6, A7, Th26;

hence Result ([x,y],M) = max ((sgn x),(sgn y)) by A8, Def9; :: thesis: verum