let X, Y, Z be non empty set ; :: thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . x,z = "\/" { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let R be RMembership_Func of X,Y; :: thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . x,z = "\/" { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let S be RMembership_Func of Y,Z; :: thesis: for x being Element of X
for z being Element of Z holds (R (#) S) . x,z = "\/" { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let x be Element of X; :: thesis: for z being Element of Z holds (R (#) S) . x,z = "\/" { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
let z be Element of Z; :: thesis: (R (#) S) . x,z = "\/" { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.])
[x,z] in [:X,Z:] ;
then A1: (R (#) S) . x,z = upper_bound (rng (min R,S,x,z)) by FUZZY_4:def 3;
set L = { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ;
A2: (R (#) S) . [x,z] is_>=_than { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum }

proof

for b being Element of (RealPoset [.0 ,1.]) st b in { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } holds
(R (#) S) . [x,z] >>= b

proof

let b be Element of (RealPoset [.0 ,1.]); :: thesis: ( b in { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } implies (R (#) S) . [x,z] >>= b )
assume b in { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ; :: thesis: (R (#) S) . [x,z] >>= b
then consider y being Element of Y such that
A3: b = (R . x,y) "/\" (S . y,z) ;
reconsider b = b as Real by Lm4;
A4: dom (min R,S,x,z) = Y by FUNCT_2:def 1;
b = (min R,S,x,z) . y by A3, FUZZY_4:def 2;
then b <= upper_bound (rng (min R,S,x,z)) by A4, FUZZY_4:1;
hence (R (#) S) . [x,z] >>= b by A1, Th3; :: thesis: verum

end;

hence (R (#) S) . [x,z] is_>=_than { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } by LATTICE3:def 9; :: thesis: verum

end;

for b being Element of (RealPoset [.0 ,1.]) st b is_>=_than { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } holds
(R (#) S) . x,z <<= b

proof

let b be Element of (RealPoset [.0 ,1.]); :: thesis: ( b is_>=_than { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } implies (R (#) S) . x,z <<= b )
assume A5: b is_>=_than { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ; :: thesis: (R (#) S) . x,z <<= b
A6: ( Y = dom (min R,S,x,z) & rng (min R,S,x,z) c= [.0 ,1.] & min R,S,x,z is PartFunc of (dom (min R,S,x,z)),(rng (min R,S,x,z)) ) by FUNCT_2:def 1, RELAT_1:def 19, RELSET_1:11;
A7: { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } = rng (min R,S,x,z) by Lm5;
A8: rng (min R,S,x,z) <> {} by Lm5;
for r being real number st r in rng (min R,S,x,z) holds
r <= b

proof

let r be real number ; :: thesis: ( r in rng (min R,S,x,z) implies r <= b )
assume A9: r in rng (min R,S,x,z) ; :: thesis: r <= b
then reconsider r = r as Element of (RealPoset [.0 ,1.]) by A6, Def3;
r <<= b by A5, A7, A9, LATTICE3:def 9;
hence r <= b by Th3; :: thesis: verum

end;

then upper_bound (rng (min R,S,x,z)) <= b by A8, TOPMETR3:1;
hence (R (#) S) . x,z <<= b by A1, Th3; :: thesis: verum

end;

hence (R (#) S) . x,z = "\/" { ((R . x,y) "/\" (S . y,z)) where y is Element of Y : verum } ,(RealPoset [.0 ,1.]) by A2, YELLOW_0:32; :: thesis: verum