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)

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

hence
o1 = o2
by MULTOP_1:3; :: thesis: verum
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;thus o1 . (a,b,c) = (a * b) + c by A2

.= o2 . (a,b,c) by A3 ; :: thesis: verum