let X be non empty set ; for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let R be RMembership_Func of X,X; for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let Q be Subset of (FuzzyLattice [:X,X:]); for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let x, z be Element of X; { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
defpred S1[ Element of X] means verum;
deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ("\/" ((pi (Q,[$1,z])),(RealPoset [.0,1.])));
deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,$1]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[$1,z]) } ,(RealPoset [.0,1.]));
for y being Element of X holds (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) = "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))
proof
let y be
Element of
X;
(R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) = "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))
FuzzyLattice [:X,X:] =
(RealPoset [.0,1.]) |^ [:X,X:]
by LFUZZY_0:def 4
.=
product ([:X,X:] --> (RealPoset [.0,1.]))
by YELLOW_1:def 5
;
then reconsider Q =
Q as
Subset of
(product ([:X,X:] --> (RealPoset [.0,1.]))) ;
pi (
Q,
[y,z]) is
Subset of
(RealPoset [.0,1.])
by FUNCOP_1:7;
hence
(R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) = "\/" (
{ ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,
(RealPoset [.0,1.]))
by Th33;
verum
end;
then A1:
for y being Element of X holds H1(y) = H2(y)
;
{ H1(y) where y is Element of X : S1[y] } = { H2(y) where y is Element of X : S1[y] }
from FRAENKEL:sch 5(A1);
hence
{ ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
; verum