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 number 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 number 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 number st z = rng f & A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
let A be real number ; :: 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

let x, y be Element of X; :: thesis: f . (x,y) <= A
f . [x,y] = f . (x,y) ;
then reconsider c = f . [x,y] as real number ;
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 5;
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