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 } ,())) 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 } ,())) where y is Element of Y : verum } ;
set D = { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ;
defpred S1[ set ] means verum;
deffunc H1( Element of Y, Element of Z) -> Element of the carrier of () = ((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 } ,())) 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 } ,())) 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 } ,())) 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 } ,())) 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 } ,()) ;
a = ((R (#) S) . (x,z)) "/\" (T . (z,w)) by ;
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 } ,())) 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 } ,()) by ;
hence a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,())) where z is Element of Z : verum } ; :: thesis: verum
end;
A7: for y being Element of Y
for z being Element of Z st S1[y] & S1[z] holds
H1(y,z) = H1(y,z) ;
A8: "\/" ( { ("\/" ( { H1(y,z) where z is Element of Z : S1[z] } ,())) where y is Element of Y : S1[y] } ,()) = "\/" ( { ("\/" ( { H1(y1,z1) where y1 is Element of Y : S1[y1] } ,())) where z1 is Element of Z : S1[z1] } ,()) from for c being object holds
( c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,())) 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 } ,())) 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 } ,())) 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 } ,())) 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 } ,()) ;
c = (R . (x,y)) "/\" ((S (#) T) . (y,w)) by ;
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 } ,())) 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 } ,()) by ;
hence c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,())) 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 } ,())) 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 } ,()) & (R (#) (S (#) T)) . (x,w) = "\/" ( { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ,()) ) by Th22;
hence ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w) by ; :: thesis: verum
end;
thus (R (#) S) (#) T = R (#) (S (#) T) by A1; :: thesis: verum