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

now :: thesis: ( dom m1 = dom m2 & ( for x being object st x in dom m1 holds
m1 . x = m2 . x ) )

dom m1 = X by PARTFUN1:def 2;
hence dom m1 = dom m2 by PARTFUN1:def 2; :: thesis: for x being object st x in dom m1 holds
m1 . x = m2 . x

hereby :: thesis: verum

let x be object ; :: thesis: ( x in dom m1 implies m1 . x = m2 . x )
assume x in dom m1 ; :: thesis: m1 . x = m2 . x
then reconsider y = x as Element of X ;
m1 . x = min ((f . y),(g . y)) by A3;
hence m1 . x = m2 . x by A4; :: thesis: verum

end;

end;

hence m1 = m2 ; :: thesis: verum