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 2 :: thesis: K73([:C1,C3:],REAL,(f (#) (min (g,h))),c) <= K73([:C1,C3:],REAL,(min ((f (#) g),(f (#) h))),c)
consider x, z being object such that
A1: x in C1 and
A2: z in C3 and
A3: c = [x,z] by ZFMISC_1:def 2;
reconsider z = z, x = x as set by TARSKI:1;
A4: (f (#) (min (g,h))) . (x,z) = upper_bound (rng (min (f,(min (g,h)),x,z))) by A3, Def3;
(min ((f (#) g),(f (#) h))) . (x,z) = min (((f (#) g) . (x,z)),((f (#) h) . (x,z))) by A3, FUZZY_1:def 3
.= min (((f (#) g) . (x,z)),(upper_bound (rng (min (f,h,x,z))))) by A3, Def3
.= min ((upper_bound (rng (min (f,g,x,z)))),(upper_bound (rng (min (f,h,x,z))))) by A3, Def3 ;
hence K73([:C1,C3:],REAL,(f (#) (min (g,h))),c) <= K73([:C1,C3:],REAL,(min ((f (#) g),(f (#) h))),c) by A1, A2, A3, A4, Lm3; :: thesis: verum