let o1, o2 be TriOp of REAL; :: thesis: ( ( for a, b, c being Real holds o1 . (a,b,c) = (a * b) + c ) & ( for a, b, c being Real holds o2 . (a,b,c) = (a * b) + c ) implies o1 = o2 )
assume that
A2: for a, b, c being Real holds o1 . (a,b,c) = (a * b) + c and
A3: for a, b, c being Real holds o2 . (a,b,c) = (a * b) + c ; :: thesis: o1 = o2
for a, b, c being Element of REAL holds o1 . (a,b,c) = o2 . (a,b,c)

proof

let a, b, c be Element of REAL ; :: thesis: o1 . (a,b,c) = o2 . (a,b,c)
thus o1 . (a,b,c) = (a * b) + c by A2
.= o2 . (a,b,c) by A3 ; :: thesis: verum

end;

hence o1 = o2 by MULTOP_1:3; :: thesis: verum