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:13;
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