let C1, C2, C3 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3 holds min (f (#) g),(f (#) h) c=
let f be RMembership_Func of C1,C2; :: thesis: for g, h being RMembership_Func of C2,C3 holds min (f (#) g),(f (#) h) c=
let g, h be RMembership_Func of C2,C3; :: thesis: min (f (#) g),(f (#) h) c=
let c be Element of [:C1,C3:]; :: according to FUZZY_1:def 3 :: thesis: (f (#) (min g,h)) . c <= (min (f (#) g),(f (#) h)) . c
consider x, z being set such that
A1: ( x in C1 & z in C3 & c = [x,z] ) by ZFMISC_1:def 2;
A2: (f (#) (min g,h)) . x,z = sup (rng (min f,(min g,h),x,z)) by A1, Def3;
(min (f (#) g),(f (#) h)) . x,z = min ((f (#) g) . x,z),((f (#) h) . x,z) by A1, FUZZY_1:def 4
.= min ((f (#) g) . x,z),(sup (rng (min f,h,x,z))) by A1, Def3
.= min (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z))) by A1, Def3 ;
hence (f (#) (min g,h)) . c <= (min (f (#) g),(f (#) h)) . c by A1, A2, Lm3; :: thesis: verum