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 A2, ZFMISC_1:87;
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 A3, ZFMISC_1:87;
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 A2, A3, FUZZY_4:18; :: thesis: verum

end;

hence S (#) U c= ; :: thesis: verum