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

(low_toler (f,A)) [*] = low_toler (f,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

(low_toler (f,A)) [*] = low_toler (f,A)

let z be non empty finite Subset of REAL; :: thesis: for A being Real st z = rng f & A >= max z holds

(low_toler (f,A)) [*] = low_toler (f,A)

let A be Real; :: thesis: ( z = rng f & A >= max z implies (low_toler (f,A)) [*] = low_toler (f,A) )

assume A1: ( z = rng f & A >= max z ) ; :: thesis: (low_toler (f,A)) [*] = low_toler (f,A)

hence (low_toler (f,A)) [*] = low_toler (f,A) by XBOOLE_0:def 10; :: thesis: verum

for z being non empty finite Subset of REAL

for A being Real st z = rng f & A >= max z holds

(low_toler (f,A)) [*] = low_toler (f,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

(low_toler (f,A)) [*] = low_toler (f,A)

let z be non empty finite Subset of REAL; :: thesis: for A being Real st z = rng f & A >= max z holds

(low_toler (f,A)) [*] = low_toler (f,A)

let A be Real; :: thesis: ( z = rng f & A >= max z implies (low_toler (f,A)) [*] = low_toler (f,A) )

assume A1: ( z = rng f & A >= max z ) ; :: thesis: (low_toler (f,A)) [*] = low_toler (f,A)

now :: thesis: for p being object st p in (low_toler (f,A)) [*] holds

p in low_toler (f,A)

then
( low_toler (f,A) c= (low_toler (f,A)) [*] & (low_toler (f,A)) [*] c= low_toler (f,A) )
by LANG1:18;p in low_toler (f,A)

let p be object ; :: thesis: ( p in (low_toler (f,A)) [*] implies p in low_toler (f,A) )

assume p in (low_toler (f,A)) [*] ; :: thesis: p in low_toler (f,A)

then consider x, y being object such that

A2: ( x in X & y in X ) and

A3: p = [x,y] by ZFMISC_1:def 2;

reconsider x9 = x, y9 = y as Element of X by A2;

f . (x9,y9) <= A by A1, Th26;

hence p in low_toler (f,A) by A3, Def3; :: thesis: verum

end;assume p in (low_toler (f,A)) [*] ; :: thesis: p in low_toler (f,A)

then consider x, y being object such that

A2: ( x in X & y in X ) and

A3: p = [x,y] by ZFMISC_1:def 2;

reconsider x9 = x, y9 = y as Element of X by A2;

f . (x9,y9) <= A by A1, Th26;

hence p in low_toler (f,A) by A3, Def3; :: thesis: verum

hence (low_toler (f,A)) [*] = low_toler (f,A) by XBOOLE_0:def 10; :: thesis: verum