let X, Y, Z be non empty set ; :: thesis: for R, S being RMembership_Func of X,Y
for T, U being RMembership_Func of Y,Z st S c= & U c= holds
S (#) U c=

let R, S be RMembership_Func of X,Y; :: thesis: for T, U being RMembership_Func of Y,Z st S c= & U c= holds
S (#) U c=

let T, U be RMembership_Func of Y,Z; :: thesis: ( S c= & U c= implies S (#) U c= )
assume A1: ( S c= & U c= ) ; :: thesis: S (#) U c=
for c being Element of [:X,Z:] holds (R (#) T) . c <= (S (#) U) . c
proof
let c be Element of [:X,Z:]; :: thesis: (R (#) T) . c <= (S (#) U) . c
consider x, z being object such that
A2: [x,z] = c by RELAT_1:def 1;
A3: ( x in X & z in Z ) by ;
for y being set st y in Y holds
( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] )
proof
let y be set ; :: thesis: ( y in Y implies ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) )
assume y in Y ; :: thesis: ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] )
then ( [x,y] in [:X,Y:] & [y,z] in [:Y,Z:] ) by ;
hence ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) by A1; :: thesis: verum
end;
hence (R (#) T) . c <= (S (#) U) . c by ; :: thesis: verum
end;
hence S (#) U c= ; :: thesis: verum