let X, Y, Z be non empty set ; :: thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0 ,1.]) holds a "/\" ((R (#) S) . x,z) = "\/" { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let R be RMembership_Func of X,Y; :: thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0 ,1.]) holds a "/\" ((R (#) S) . x,z) = "\/" { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let S be RMembership_Func of Y,Z; :: thesis: for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0 ,1.]) holds a "/\" ((R (#) S) . x,z) = "\/" { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let x be Element of X; :: thesis: for z being Element of Z
for a being Element of (RealPoset [.0 ,1.]) holds a "/\" ((R (#) S) . x,z) = "\/" { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let z be Element of Z; :: thesis: for a being Element of (RealPoset [.0 ,1.]) holds a "/\" ((R (#) S) . x,z) = "\/" { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let a be Element of (RealPoset [.0 ,1.]); :: thesis: a "/\" ((R (#) S) . x,z) = "\/" { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
set A = { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ;
set B = { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } ;
for b being set holds
( b in { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } iff b in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } )

proof

let b be set ; :: thesis: ( b in { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } iff b in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } )

hereby :: thesis: ( b in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } implies b in { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } )

assume b in { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ; :: thesis: b in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum }
then consider y being Element of Y such that
A1: b = (a "/\" (R . x,y)) "/\" (S . y,z) ;
b = ((R . x,y) "/\" (S . y,z)) "/\" a by A1, LATTICE3:16;
hence b in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } ; :: thesis: verum

end;

assume b in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } ; :: thesis: b in { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum }
then consider y being Element of Y such that
A2: b = ((R . x,y) "/\" (S . y,z)) "/\" a ;
b = (a "/\" (R . x,y)) "/\" (S . y,z) by A2, LATTICE3:16;
hence b in { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ; :: thesis: verum

end;

then { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } = { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } by TARSKI:2;
hence a "/\" ((R (#) S) . x,z) = "\/" { ((a "/\" (R . x,y)) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.]) by Lm6; :: thesis: verum