let r be Real; :: thesis: for X being non empty set
for f being Function of [:X,X:],REAL
for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y)))
let X be non empty set ; :: thesis: for f being Function of [:X,X:],REAL
for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y)))
let f be Function of [:X,X:],REAL; :: thesis: for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y)))
let x, y be Element of X; :: thesis: (min (r,f)) . (x,y) = min (r,(f . (x,y)))
(min (r,f)) . (x,y) = min (r,(f . [x,y])) by Def9;
hence (min (r,f)) . (x,y) = min (r,(f . (x,y))) ; :: thesis: verum