let C1, C2, C3 be non empty set ; 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; for h being RMembership_Func of C2,C3 holds min ((f (#) h),(g (#) h)) c=
let h be RMembership_Func of C2,C3; min ((f (#) h),(g (#) h)) c=
let c be Element of [:C1,C3:]; FUZZY_1:def 2 K73([:C1,C3:],REAL,((min (f,g)) (#) h),c) <= K73([:C1,C3:],REAL,(min ((f (#) h),(g (#) 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:
((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 3
.=
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
K73([:C1,C3:],REAL,((min (f,g)) (#) h),c) <= K73([:C1,C3:],REAL,(min ((f (#) h),(g (#) h))),c)
by A1, A2, A3, A4, Lm4; verum