let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds R (#) (@ ("\/" Q,(FuzzyLattice [:X,X:]))) = "\/" { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])
let R be RMembership_Func of X,X; :: thesis: for Q being Subset of (FuzzyLattice [:X,X:]) holds R (#) (@ ("\/" Q,(FuzzyLattice [:X,X:]))) = "\/" { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])
let Q be Subset of (FuzzyLattice [:X,X:]); :: thesis: R (#) (@ ("\/" Q,(FuzzyLattice [:X,X:]))) = "\/" { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])
set FL = FuzzyLattice [:X,X:];
set RP = RealPoset [.0 ,1.];
"\/" { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]) = @ ("\/" { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) by LFUZZY_0:def 5;
then reconsider F = "\/" { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]) as RMembership_Func of X,X ;
for x, z being Element of X holds (R (#) (@ ("\/" Q,(FuzzyLattice [:X,X:])))) . x,z = F . x,z

proof

let x, z be Element of X; :: thesis: (R (#) (@ ("\/" Q,(FuzzyLattice [:X,X:])))) . x,z = F . x,z
A1: { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= the carrier of (FuzzyLattice [:X,X:])

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: t in the carrier of (FuzzyLattice [:X,X:])
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A2: t = R (#) (@ r) and
r in Q ;
[:X,X:],(R (#) (@ r)) @ = R (#) (@ r) by LFUZZY_0:def 6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; :: thesis: verum

end;

thus (R (#) (@ ("\/" Q,(FuzzyLattice [:X,X:])))) . x,z = "\/" { ((R . x,y) "/\" ((@ ("\/" Q,(FuzzyLattice [:X,X:]))) . y,z)) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) by LFUZZY_0:22
.= "\/" { ((R . [x,y]) "/\" ("\/" (pi Q,[y,z]),(RealPoset [.0 ,1.]))) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) by Lm2
.= "\/" { ("\/" { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0 ,1.]) : b in pi Q,[y,z] } ,(RealPoset [.0 ,1.])) where y is Element of X : verum } ,(RealPoset [.0 ,1.]) by Lm3
.= "\/" { ("\/" { ((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.]) by Lm4
.= "\/" { ("\/" { ((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 } ,(RealPoset [.0 ,1.]) by Lm10
.= "\/" { ("\/" { ((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 } ,(RealPoset [.0 ,1.]) by Lm7
.= "\/" { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0 ,1.]) by Lm8
.= "\/" (pi { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]),(RealPoset [.0 ,1.]) by Lm9
.= F . x,z by A1, Th32 ; :: thesis: verum

end;

hence R (#) (@ ("\/" Q,(FuzzyLattice [:X,X:]))) = "\/" { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]) by Th2; :: thesis: verum