let X, Y, Z, W be non empty set ; :: thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let R be RMembership_Func of X,Y; :: thesis: for S being RMembership_Func of Y,Z
for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let S be RMembership_Func of Y,Z; :: thesis: for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let T be RMembership_Func of Z,W; :: thesis: (R (#) S) (#) T = R (#) (S (#) T)
A1: for x, w being set st x in X & w in W holds
((R (#) S) (#) T) . x,w = (R (#) (S (#) T)) . x,w

proof

let x, w be set ; :: thesis: ( x in X & w in W implies ((R (#) S) (#) T) . x,w = (R (#) (S (#) T)) . x,w )
assume that
A2: x in X and
A3: w in W ; :: thesis: ((R (#) S) (#) T) . x,w = (R (#) (S (#) T)) . x,w
reconsider w = w as Element of W by A3;
reconsider x = x as Element of X by A2;
set A = { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])) where z is Element of Z : verum } ;
set B = { (((R (#) S) . x,z) "/\" (T . z,w)) where z is Element of Z : verum } ;
set C = { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.])) where y is Element of Y : verum } ;
set D = { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum } ;
defpred S₁[ set ] means verum;
deffunc H₁( Element of Y, Element of Z) -> Element of the carrier of (RealPoset [.0 ,1.]) = ((R . x,$1) "/\" (S . $1,$2)) "/\" (T . $2,w);
A4: for a being set holds
( a in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])) where z is Element of Z : verum } iff a in { (((R (#) S) . x,z) "/\" (T . z,w)) where z is Element of Z : verum } )

proof

let a be set ; :: thesis: ( a in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])) where z is Element of Z : verum } iff a in { (((R (#) S) . x,z) "/\" (T . z,w)) where z is Element of Z : verum } )

hereby :: thesis: ( a in { (((R (#) S) . x,z) "/\" (T . z,w)) where z is Element of Z : verum } implies a in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])) where z is Element of Z : verum } )

assume a in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])) where z is Element of Z : verum } ; :: thesis: a in { (((R (#) S) . x,z) "/\" (T . z,w)) where z is Element of Z : verum }
then consider z being Element of Z such that
A5: a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.]) ;
a = ((R (#) S) . x,z) "/\" (T . z,w) by A5, Lm6;
hence a in { (((R (#) S) . x,z) "/\" (T . z,w)) where z is Element of Z : verum } ; :: thesis: verum

end;

assume a in { (((R (#) S) . x,z) "/\" (T . z,w)) where z is Element of Z : verum } ; :: thesis: a in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])) where z is Element of Z : verum }
then consider z being Element of Z such that
A6: a = ((R (#) S) . x,z) "/\" (T . z,w) ;
a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.]) by A6, Lm6;
hence a in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])) where z is Element of Z : verum } ; :: thesis: verum

end;

A7: for y being Element of Y
for z being Element of Z st S₁[y] & S₁[z] holds
H₁(y,z) = H₁(y,z) ;
A8: "\/" { ("\/" { H₁(y,z) where z is Element of Z : S₁[z] } ,(RealPoset [.0 ,1.])) where y is Element of Y : S₁[y] } ,(RealPoset [.0 ,1.]) = "\/" { ("\/" { H₁(y1,z1) where y1 is Element of Y : S₁[y1] } ,(RealPoset [.0 ,1.])) where z1 is Element of Z : S₁[z1] } ,(RealPoset [.0 ,1.]) from LFUZZY_0:sch 5(A7);
for c being set holds
( c in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.])) where y is Element of Y : verum } iff c in { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum } )

proof

let c be set ; :: thesis: ( c in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.])) where y is Element of Y : verum } iff c in { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum } )

hereby :: thesis: ( c in { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum } implies c in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.])) where y is Element of Y : verum } )

assume c in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.])) where y is Element of Y : verum } ; :: thesis: c in { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum }
then consider y being Element of Y such that
A9: c = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.]) ;
c = (R . x,y) "/\" ((S (#) T) . y,w) by A9, Lm7;
hence c in { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum } ; :: thesis: verum

end;

assume c in { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum } ; :: thesis: c in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.])) where y is Element of Y : verum }
then consider y being Element of Y such that
A10: c = (R . x,y) "/\" ((S (#) T) . y,w) ;
c = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.]) by A10, Lm7;
hence c in { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.])) where y is Element of Y : verum } ; :: thesis: verum

end;

then A11: { ("\/" { (((R . x,y) "/\" (S . y,z)) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.])) where y is Element of Y : verum } = { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum } by TARSKI:2;
( ((R (#) S) (#) T) . x,w = "\/" { (((R (#) S) . x,z) "/\" (T . z,w)) where z is Element of Z : verum } ,(RealPoset [.0 ,1.]) & (R (#) (S (#) T)) . x,w = "\/" { ((R . x,y) "/\" ((S (#) T) . y,w)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.]) ) by Th22;
hence ((R (#) S) (#) T) . x,w = (R (#) (S (#) T)) . x,w by A4, A11, A8, TARSKI:2; :: thesis: verum

end;

( dom ((R (#) S) (#) T) = [:X,W:] & dom (R (#) (S (#) T)) = [:X,W:] ) by FUNCT_2:def 1;
hence (R (#) S) (#) T = R (#) (S (#) T) by A1, FUNCT_3:6; :: thesis: verum