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 :: thesis: for x being object st x in X holds
M1 . x = M2 . x

let x be object ; :: 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) by A3, A5;
hence M1 . x = M2 . x by A4, A5; :: thesis: verum

end;

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