let m1, m2 be Function of X,REAL; ( ( for x being Element of X holds m1 . x = max ((f . x),(g . x)) ) & ( for x being Element of X holds m2 . x = max ((f . x),(g . x)) ) implies m1 = m2 )
assume that
A3:
for x being Element of X holds m1 . x = max ((f . x),(g . x))
and
A4:
for x being Element of X holds m2 . x = max ((f . x),(g . x))
; m1 = m2
hence
m1 = m2
; verum