let X be non empty set ; :: thesis: 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; :: thesis: 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:]); :: thesis: 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; :: thesis: { ((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 S₁[ Element of X] means verum;
deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ("\/" ((pi (Q,[$1,z])),(RealPoset [.0,1.])));
deffunc H₂( 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; :: thesis: (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; :: thesis: verum

end;

then A1: for y being Element of X holds H₁(y) = H₂(y) ;
{ H₁(y) where y is Element of X : S₁[y] } = { H₂(y) where y is Element of X : S₁[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 } ; :: thesis: verum