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 ((R (#) S) . x,z) "/\" a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" a) 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 ((R (#) S) . x,z) "/\" a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" a) 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 ((R (#) S) . x,z) "/\" a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" a) 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 ((R (#) S) . x,z) "/\" a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" a) 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 ((R (#) S) . x,z) "/\" a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let a be Element of (RealPoset [.0 ,1.]); :: thesis: ((R (#) S) . x,z) "/\" a = "\/" { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
A1: { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } c= the carrier of (RealPoset [.0 ,1.])

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } or d in the carrier of (RealPoset [.0 ,1.]) )
assume d in { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ; :: thesis: d in the carrier of (RealPoset [.0 ,1.])
then ex t being Element of Y st d = (R . x,t) "/\" (S . t,z) ;
hence d in the carrier of (RealPoset [.0 ,1.]) ; :: thesis: verum

end;

set A = { (b "/\" a) where b is Element of (RealPoset [.0 ,1.]) : b in { ((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 } ;
A2: for c being set holds
( c in { (b "/\" a) where b is Element of (RealPoset [.0 ,1.]) : b in { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } } iff c in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } )

proof

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

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

assume c in { (b "/\" a) where b is Element of (RealPoset [.0 ,1.]) : b in { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } } ; :: thesis: c in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum }
then consider b being Element of (RealPoset [.0 ,1.]) such that
A3: c = b "/\" a and
A4: b in { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ;
ex y being Element of Y st b = (R . x,y) "/\" (S . y,z) by A4;
hence c in { (((R . x,y) "/\" (S . y,z)) "/\" a) where y is Element of Y : verum } by A3; :: thesis: verum

end;

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

end;

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