let M1, M2 be Function of X,REAL ; :: thesis: ( ( for x being set st x in X holds
M1 . x = min r,(f . x) ) & ( for x being set st x in X holds
M2 . x = min r,(f . x) ) implies M1 = M2 )
assume that
A3: for x being set st x in X holds
M1 . x = min r,(f . x) and
A4: for x being set st x in X holds
M2 . x = min r,(f . x) ; :: thesis: M1 = M2

now

let x be set ; :: thesis: ( x in X implies M1 . x = M2 . x )
assume A5: x in X ; :: thesis: M1 . x = M2 . x
reconsider y = x as Element of X by A5;
( M1 . x = H₁(y) & M2 . x = H₁(y) ) by A3, A4, A5;
hence M1 . x = M2 . x ; :: thesis: verum

end;

hence M1 = M2 by FUNCT_2:18; :: thesis: verum