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 object st x in X & w in W holds
((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w)

proof

let x, w be object ; :: 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 object 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 object ; :: 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, Lm5;
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, Lm5;
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 object 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 object ; :: 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, Lm6;
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, Lm6;
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;

thus (R (#) S) (#) T = R (#) (S (#) T) by A1; :: thesis: verum