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