deffunc H₁( 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₁(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₁(a,b,c) by A1;
hence X . (a,b,c) = (a * b) + c ; :: thesis: verum