let X be non empty finite Subset of REAL; :: thesis: for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being Real st z = rng f & A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
let f be Function of [:X,X:],REAL; :: thesis: for z being non empty finite Subset of REAL
for A being Real st z = rng f & A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
let z be non empty finite Subset of REAL; :: thesis: for A being Real st z = rng f & A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
let A be Real; :: thesis: ( z = rng f & A >= max z implies for x, y being Element of X holds f . (x,y) <= A )
assume that
A1: z = rng f and
A2: A >= max z ; :: thesis: for x, y being Element of X holds f . (x,y) <= A

now :: thesis: for x, y being Element of X holds f . (x,y) <= A

let x, y be Element of X; :: thesis: f . (x,y) <= A
reconsider c = f . [x,y] as Real ;
dom f = [:X,X:] by FUNCT_2:def 1;
then [x,y] in dom f by ZFMISC_1:def 2;
then c in z by A1, FUNCT_1:def 3;
then f . (x,y) <= max z by XXREAL_2:def 8;
hence f . (x,y) <= A by A2, XXREAL_0:2; :: thesis: verum

end;

hence for x, y being Element of X holds f . (x,y) <= A ; :: thesis: verum