let X be non empty finite Subset of REAL; 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; 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; for A being Real st z = rng f & A >= max z holds
(low_toler (f,A)) [*] = low_toler (f,A)
let A be Real; ( z = rng f & A >= max z implies (low_toler (f,A)) [*] = low_toler (f,A) )
assume A1:
( z = rng f & A >= max z )
; (low_toler (f,A)) [*] = low_toler (f,A)
now for p being object st p in (low_toler (f,A)) [*] holds
p in low_toler (f,A)let p be
object ;
( p in (low_toler (f,A)) [*] implies p in low_toler (f,A) )assume
p in (low_toler (f,A)) [*]
;
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;
verum end;
then
( low_toler (f,A) c= (low_toler (f,A)) [*] & (low_toler (f,A)) [*] c= low_toler (f,A) )
by LANG1:18;
hence
(low_toler (f,A)) [*] = low_toler (f,A)
by XBOOLE_0:def 10; verum