let M be non empty calculating_type halting Moore-SM_Final of [: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 A1: ( 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 ) ; :: 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 A2: ( ( 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 ) ) ; :: thesis: for x, y being Element of REAL holds Result [x,y],M = max (sgn x),(sgn y)
let x, y be Real; :: thesis: Result [x,y],M = max (sgn x),(sgn y)
( max (sgn x),(sgn y) in succ REAL & [x,y] leads_to_final_state_of M & max (sgn x),(sgn y) is_result_of [x,y],M ) by A1, A2, Def6, Th26, XBOOLE_0:def 3;
hence Result [x,y],M = max (sgn x),(sgn y) by Def9; :: thesis: verum