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