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

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

hence
S (#) U c=
; :: thesis: verum
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] )

end;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

hence
(R (#) T) . c <= (S (#) U) . c
by A2, A3, FUZZY_4:18; :: thesis: verum
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;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