let C1, C2, C3 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2
for h, k being RMembership_Func of C2,C3 st g c= & k c= holds
g (#) k c=
let f, g be RMembership_Func of C1,C2; :: thesis: for h, k being RMembership_Func of C2,C3 st g c= & k c= holds
g (#) k c=
let h, k be RMembership_Func of C2,C3; :: thesis: ( g c= & k c= implies g (#) k c= )
assume that
A1: g c= and
A2: k c= ; :: thesis: g (#) k c=
let c be Element of [:C1,C3:]; :: according to FUZZY_1:def 2 :: thesis: K73([:C1,C3:],REAL,(f (#) h),c) <= K73([:C1,C3:],REAL,(g (#) k),c)
consider x, z being object such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] )

proof

let y be set ; :: thesis: ( y in C2 implies ( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) )
assume A6: y in C2 ; :: thesis: ( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] )
then A7: [y,z] in [:C2,C3:] by A4, ZFMISC_1:87;
[x,y] in [:C1,C2:] by A3, A6, ZFMISC_1:87;
hence ( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) by A1, A2, A7; :: thesis: verum

end;

hence K73([:C1,C3:],REAL,(f (#) h),c) <= K73([:C1,C3:],REAL,(g (#) k),c) by A3, A4, A5, Th18; :: thesis: verum