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)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y 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)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y 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)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }
let x, z be Element of X; :: thesis: { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y 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)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . ($1,z));
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ("\/" ((pi (Q,[$1,z])),(RealPoset [.0,1.])));
for y being Element of X holds (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))

proof

let y be Element of X; :: thesis: (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))
(@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z] = ("\/" (Q,(FuzzyLattice [:X,X:]))) . [y,z] by LFUZZY_0:def 5
.= "\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])) by Th32 ;
hence (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) ; :: thesis: verum

end;

then A1: for y being Element of X holds H₁(y) = H₂(y) ;
thus { H₁(y) where y is Element of X : S₁[y] } = { H₂(y9) where y9 is Element of X : S₁[y9] } from FRAENKEL:sch 5(A1); :: thesis: verum