let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ 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 (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ 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: (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ 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 ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = F . (x,z)

proof

let x, z be Element of X; :: thesis: ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (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 object ; :: 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;

A3: { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" ( { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y9]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }

proof

deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (b "/\" (R . [$1,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,$1]) } ,(RealPoset [.0,1.]));
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ("\/" ((pi (Q,[x,$1])),(RealPoset [.0,1.]))) "/\" (R . [$1,z]);
defpred S₁[ Element of X] means verum;
for y being Element of X holds ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.]))

proof

FuzzyLattice [:X,X:] = (RealPoset [.0,1.]) |^ [:X,X:] by LFUZZY_0:def 4
.= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def 5 ;
then reconsider Q = Q as Subset of (product ([:X,X:] --> (RealPoset [.0,1.]))) ;
let y be Element of X; :: thesis: ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.]))
pi (Q,[x,y]) is Subset of (RealPoset [.0,1.]) by FUNCOP_1:7;
hence ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) by LFUZZY_0:15; :: thesis: verum

end;

then A4: for y being Element of X holds H₂(y) = H₁(y) ;
{ H₂(y) where y is Element of X : S₁[y] } = { H₁(y9) where y9 is Element of X : S₁[y9] } from FRAENKEL:sch 5(A4);
hence { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" ( { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y9]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } ; :: thesis: verum

end;

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

proof

let y be Element of X; :: thesis: "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))
set A = { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ;
set B = { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
A6: { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } )
assume a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A7: a = (r . [x,y]) "/\" (R . [y,z]) and
A8: r in Q ;
r . [x,y] in pi (Q,[x,y]) by A8, CARD_3:def 6;
hence a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } by A7; :: thesis: verum

end;

{ (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } c= { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } or a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ; :: thesis: a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider b being Element of (RealPoset [.0,1.]) such that
A9: a = b "/\" (R . [y,z]) and
A10: b in pi (Q,[x,y]) ;
ex f being Function st
( f in Q & b = f . [x,y] ) by A10, CARD_3:def 6;
hence a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A9; :: thesis: verum

end;

hence "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by A6, XBOOLE_0:def 10; :: thesis: verum

end;

then A11: for y being Element of X holds H₂(y) = H₁(y) ;
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(A11); :: thesis: verum

end;

A12: "\/" ( { ("\/" ( { ((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.])) = "\/" ( { ("\/" ( { ((r9 . [x,y]) "/\" (R . [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.]))

proof

deffunc H₁( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = ($2 . [x,$1]) "/\" (R . [$1,z]);
defpred S₁[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
defpred S₂[ Element of X] means verum;
A13: 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(A13); :: thesis: verum

end;

A14: { ("\/" ( { ((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 } = { ("\/" ( { (((@ r9) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }

proof

deffunc H₁( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (((@ $1) . [x,y]) "/\" (R . [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.]) = "\/" ( { (($1 . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]));
defpred S₁[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
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;
A15: 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(A15); :: 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 A16: 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(A16); :: thesis: verum

end;

A17: { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])

proof

set A = { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
set B = pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]);
thus { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) :: according to XBOOLE_0:def 10 :: thesis: pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) )
assume a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; :: thesis: a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A18: a = ((@ r) (#) R) . [x,z] and
A19: r in Q ;
(@ r) (#) R in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } by A19;
hence a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) by A18, CARD_3:def 6; :: thesis: verum

end;

thus pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } :: thesis: verum

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) or b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ; :: thesis: b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider f being Function such that
A20: f in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } and
A21: b = f . [x,z] by CARD_3:def 6;
ex r being Element of (FuzzyLattice [:X,X:]) st
( f = (@ r) (#) R & r in Q ) by A20;
hence b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A21; :: thesis: verum

end;

end;

A22: { (((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum }

proof

deffunc H₁( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ("\/" ((pi (Q,[x,$1])),(RealPoset [.0,1.]))) "/\" (R . [$1,z]);
deffunc H₂( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,$1]) "/\" (R . [$1,z]);
defpred S₁[ Element of X] means verum;
for y being Element of X holds ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z]) = ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])

proof

let y be Element of X; :: thesis: ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z]) = ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])
(@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y] = ("\/" (Q,(FuzzyLattice [:X,X:]))) . [x,y] by LFUZZY_0:def 5
.= "\/" ((pi (Q,[x,y])),(RealPoset [.0,1.])) by Th32 ;
hence ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z]) = ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) ; :: thesis: verum

end;

then A23: for y being Element of X holds H₂(y) = H₁(y) ;
thus { H₂(y) where y is Element of X : S₁[y] } = { H₁(y9) where y9 is Element of X : S₁[y9] } from FRAENKEL:sch 5(A23); :: thesis: verum

end;

A24: { ("\/" ( { (((@ 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 } = { (((@ r9) (#) R) . [x,z]) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }

proof

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

end;

thus ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = "\/" ( { (((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm6
.= F . (x,z) by A1, A22, A3, A5, A12, A14, A24, A17, Th32 ; :: thesis: verum

end;

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