let X be non empty set ; :: thesis: for f being PartFunc of [:X,X:],REAL st f is nonnegative & f is Reflexive & f is discerning holds

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

let f be PartFunc of [:X,X:],REAL; :: thesis: ( f is nonnegative & f is Reflexive & f is discerning implies (low_toler (f,0)) [*] = low_toler (f,0) )

assume A1: ( f is nonnegative & f is Reflexive & f is discerning ) ; :: thesis: (low_toler (f,0)) [*] = low_toler (f,0)

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

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

let f be PartFunc of [:X,X:],REAL; :: thesis: ( f is nonnegative & f is Reflexive & f is discerning implies (low_toler (f,0)) [*] = low_toler (f,0) )

assume A1: ( f is nonnegative & f is Reflexive & f is discerning ) ; :: thesis: (low_toler (f,0)) [*] = low_toler (f,0)

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

p in low_toler (f,0)

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

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

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

consider x, y being object such that

A3: p = [x,y] by A2, RELAT_1:def 1;

low_toler (f,0) reduces x,y by A2, A3, REWRITE1:20;

then consider r being RedSequence of low_toler (f,0) such that

A4: ( r . 1 = x & r . (len r) = y ) by REWRITE1:def 3;

0 < len r by REWRITE1:def 2;

then 0 + 1 <= len r by NAT_1:13;

then ( 1 in dom r & len r in dom r ) by FINSEQ_3:25;

then r . 1 = r . (len r) by A5, Th2;

hence p in low_toler (f,0) by A1, A3, A4, A6, Th21; :: thesis: verum

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

consider x, y being object such that

A3: p = [x,y] by A2, RELAT_1:def 1;

low_toler (f,0) reduces x,y by A2, A3, REWRITE1:20;

then consider r being RedSequence of low_toler (f,0) such that

A4: ( r . 1 = x & r . (len r) = y ) by REWRITE1:def 3;

A5: now :: thesis: for i being Nat st i in dom r & i + 1 in dom r holds

r . i = r . (i + 1)

A6:
x is Element of X
by A2, A3, ZFMISC_1:87;r . i = r . (i + 1)

let i be Nat; :: thesis: ( i in dom r & i + 1 in dom r implies r . i = r . (i + 1) )

assume ( i in dom r & i + 1 in dom r ) ; :: thesis: r . i = r . (i + 1)

then [(r . i),(r . (i + 1))] in low_toler (f,0) by REWRITE1:def 2;

hence r . i = r . (i + 1) by A1, Th20; :: thesis: verum

end;assume ( i in dom r & i + 1 in dom r ) ; :: thesis: r . i = r . (i + 1)

then [(r . i),(r . (i + 1))] in low_toler (f,0) by REWRITE1:def 2;

hence r . i = r . (i + 1) by A1, Th20; :: thesis: verum

0 < len r by REWRITE1:def 2;

then 0 + 1 <= len r by NAT_1:13;

then ( 1 in dom r & len r in dom r ) by FINSEQ_3:25;

then r . 1 = r . (len r) by A5, Th2;

hence p in low_toler (f,0) by A1, A3, A4, A6, Th21; :: thesis: verum

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