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