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

proof

let r be Element of (FuzzyLattice [:X,X:]); :: thesis: ( r in Q implies "\/" { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) )
assume r in Q ; :: thesis: "\/" { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.])
{ ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } = { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum }

proof

deffunc H₃( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = (R . [x,$1]) "/\" ((@ r) . [$1,z]);
deffunc H₄( Element of X) -> Element of the carrier of (RealPoset [.0 ,1.]) = (R . [x,$1]) "/\" (r . [$1,z]);
defpred S₂[ Element of X] means verum;
A1: for y being Element of X holds H₄(y) = H₃(y) by LFUZZY_0:def 5;
thus { 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); :: thesis: verum

end;

hence "\/" { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) = "\/" { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) ; :: thesis: verum

end;

then A2: for r being Element of (FuzzyLattice [:X,X:]) st S₁[r] holds
H₁(r) = H₂(r) ;
thus { H₁(r) where r is Element of (FuzzyLattice [:X,X:]) : S₁[r] } = { H₂(r) where r is Element of (FuzzyLattice [:X,X:]) : S₁[r] } from FRAENKEL:sch 6(A2); :: thesis: verum