deffunc H1( Real, Real) -> Element of REAL = In ((max ($1,$2)),REAL);
consider f being BinOp of REAL such that
A1:
for x, y being Element of REAL holds f . (x,y) = H1(x,y)
from BINOP_1:sch 4();
A2:
for x, y being Element of REAL holds f . (x,y) = max (x,y)
let M be non empty Moore-SM_Final over [:REAL,REAL:], succ REAL; ( 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 >= y holds
the Tran of M . [ the InitS of M,[x,y]] = x ) & ( for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = y ) implies for x, y being Element of REAL holds max (x,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
; ( ex x, y being Real st
( x >= y & not the Tran of M . [ the InitS of M,[x,y]] = x ) or ex x, y being Real st
( x < y & not the Tran of M . [ the InitS of M,[x,y]] = y ) or for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M )
assume that
A8:
for x, y being Real st x >= y holds
the Tran of M . [ the InitS of M,[x,y]] = x
and
A9:
for x, y being Real st x < y holds
the Tran of M . [ the InitS of M,[x,y]] = y
; for x, y being Element of REAL holds max (x,y) is_result_of [x,y],M
let x, y be Element of REAL ; max (x,y) is_result_of [x,y],M
reconsider x = x, y = y as Element of REAL ;
now for x, y being Element of REAL holds the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)let x,
y be
Element of
REAL ;
the Tran of M . [ the InitS of M,[x,y]] = f . (x,y)A10:
(
x >= y implies the
Tran of
M . [ the InitS of M,[x,y]] = x )
by A8;
(
x < y implies the
Tran of
M . [ the InitS of M,[x,y]] = y )
by A9;
then
the
Tran of
M . [ the InitS of M,[x,y]] = max (
x,
y)
by A10, XXREAL_0:def 10;
hence
the
Tran of
M . [ the InitS of M,[x,y]] = f . (
x,
y)
by A2;
verum end;
then
f . (x,y) is_result_of [x,y],M
by A3, A4, A5, A6, A7, Th22;
hence
max (x,y) is_result_of [x,y],M
by A2; verum