let F1, F2 be BinOp of (Funcs A,REAL ); :: thesis: ( ( for f, g being Element of Funcs A,REAL holds F1 . f,g = maxreal .: f,g ) & ( for f, g being Element of Funcs A,REAL holds F2 . f,g = maxreal .: f,g ) implies F1 = F2 )
assume that
A1: for f, g being Element of Funcs A,REAL holds F1 . f,g = maxreal .: f,g and
A2: for f, g being Element of Funcs A,REAL holds F2 . f,g = maxreal .: f,g ; :: thesis: F1 = F2

now

let f, g be Element of Funcs A,REAL ; :: thesis: F1 . f,g = F2 . f,g
thus F1 . f,g = maxreal .: f,g by A1
.= F2 . f,g by A2 ; :: thesis: verum

end;

hence F1 = F2 by BINOP_1:2; :: thesis: verum