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

now

let p be set ; :: 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 set such that
A3: p = [x,y] by A2, RELAT_1:def 1;
low_toler f,0 reduces x,y by A2, A3, REWRITE1:21;
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

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;

A6: x is Element of X by A2, A3, ZFMISC_1:106;
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:27;
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;

then ( low_toler f,0 c= (low_toler f,0 ) [*] & (low_toler f,0 ) [*] c= low_toler f,0 ) by LANG1:18, TARSKI:def 3;
hence (low_toler f,0 ) [*] = low_toler f,0 by XBOOLE_0:def 10; :: thesis: verum