theorem Th26:
for
M being non
empty Moore-SM_Final over
[:REAL,REAL:],
succ REAL st
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
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 ) holds
for
x,
y being
Element of
REAL holds
max (
(sgn x),
(sgn y))
is_result_of [x,y],
M