deffunc H₁( Real, Real) -> Element of REAL = $1 + $2;
consider f being BinOp of REAL such that
A1: for x, y being Real holds f . (x,y) = H₁(x,y) from BINOP_1:sch 4();
let M be non empty Moore-SM_Final of [: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 holds the Tran of M . [ the InitS of M,[x,y]] = x + y ) implies for x, y being Element of REAL holds x + y is_result_of [x,y],M )
assume that
A2: M is calculating_type and
A3: the carrier of M = succ REAL and
A4: the FinalS of M = REAL and
A5: the InitS of M = REAL and
A6: the OFun of M = id the carrier of M ; :: thesis: ( ex x, y being Real st not the Tran of M . [ the InitS of M,[x,y]] = x + y or for x, y being Element of REAL holds x + y is_result_of [x,y],M )
assume A7: for x, y being Real holds the Tran of M . [ the InitS of M,[x,y]] = x + y ; :: thesis: for x, y being Element of REAL holds x + y is_result_of [x,y],M
let x, y be Real; :: thesis: x + y is_result_of [x,y],M

now

let x, y be 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]] = x + y by A7;
hence the Tran of M . [ the InitS of M,[x,y]] = f . (x,y) by A1; :: thesis: verum

end;

then f . (x,y) is_result_of [x,y],M by A2, A3, A4, A5, A6, Th22;
hence x + y is_result_of [x,y],M by A1; :: thesis: verum