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

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