let F1, F2 be BinOp of (Funcs (A,REAL)); :: thesis: ( ( for f, g being Element of Funcs (A,REAL) holds F1 . (f,g) = minreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds F2 . (f,g) = minreal .: (f,g) ) implies F1 = F2 )
assume that
A3: for f, g being Element of Funcs (A,REAL) holds F1 . (f,g) = minreal .: (f,g) and
A4: for f, g being Element of Funcs (A,REAL) holds F2 . (f,g) = minreal .: (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) = minreal .: (f,g) by A3
.= F2 . (f,g) by A4 ; :: thesis: verum
end;
hence F1 = F2 by BINOP_1:2; :: thesis: verum