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:4; :: thesis: verum