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 :: thesis: for f, g being Element of Funcs (A,REAL) holds F1 . (f,g) = F2 . (f,g)

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