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
A1: for a, b, c being Real holds o1 . (a,b,c) = (a * b) + c and
A2: for a, b, c being Real holds o2 . (a,b,c) = (a * b) + c ; :: thesis: o1 = o2
for a, b, c being Real holds o1 . (a,b,c) = o2 . (a,b,c)

proof

let a, b, c be Real; :: thesis: o1 . (a,b,c) = o2 . (a,b,c)
thus o1 . (a,b,c) = (a * b) + c by A1
.= o2 . (a,b,c) by A2 ; :: thesis: verum

end;

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