deffunc H_{1}( Real, Real, Real) -> Element of REAL = In ((($1 * $2) + $3),REAL);

consider X being TriOp of REAL such that

A1: for a, b, c being Element of REAL holds X . (a,b,c) = H_{1}(a,b,c)
from MULTOP_1:sch 4();

take X ; :: thesis: for a, b, c being Real holds X . (a,b,c) = (a * b) + c

let a, b, c be Real; :: thesis: X . (a,b,c) = (a * b) + c

reconsider a = a, b = b, c = c as Element of REAL by XREAL_0:def 1;

X . (a,b,c) = H_{1}(a,b,c)
by A1;

hence X . (a,b,c) = (a * b) + c ; :: thesis: verum

consider X being TriOp of REAL such that

A1: for a, b, c being Element of REAL holds X . (a,b,c) = H

take X ; :: thesis: for a, b, c being Real holds X . (a,b,c) = (a * b) + c

let a, b, c be Real; :: thesis: X . (a,b,c) = (a * b) + c

reconsider a = a, b = b, c = c as Element of REAL by XREAL_0:def 1;

X . (a,b,c) = H

hence X . (a,b,c) = (a * b) + c ; :: thesis: verum