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