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 S1[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
deffunc H1( 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 H2( 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 H3( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ((@ r) . [$1,z]);
deffunc H4( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" (r . [$1,z]);
defpred S2[ Element of X] means verum;
A1: for y being Element of X holds H4(y) = H3(y) by LFUZZY_0:def 5;
thus { H4(y) where y is Element of X : S2[y] } = { H3(y) where y is Element of X : S2[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 S1[r] holds
H1(r) = H2(r) ;
thus { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch 6(A2); :: thesis: verum