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 :: thesis: for p being object st p in (low_toler (f,0)) [*] holds
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;
A5: now :: thesis: for i being Nat st i in dom r & i + 1 in dom r holds
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;
A6: x is Element of X by A2, A3, ZFMISC_1:87;
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;
then ( low_toler (f,0) c= (low_toler (f,0)) [*] & (low_toler (f,0)) [*] c= low_toler (f,0) ) by LANG1:18;
hence (low_toler (f,0)) [*] = low_toler (f,0) by XBOOLE_0:def 10; :: thesis: verum