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

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

hence
for x, y being Element of X holds f . (x,y) <= A
; :: thesis: verumlet 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;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