let X, Y, Z be non empty set ; 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; 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; ( S c= & U c= implies S (#) U c= )
assume A1:
( S c= & U c= )
; 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:];
(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 ;
( y in Y implies ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) )
assume
y in Y
;
( 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;
verum
end;
hence
(R (#) T) . c <= (S (#) U) . c
by A2, A3, FUZZY_4:18;
verum
end;
hence
S (#) U c=
; verum