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 } ,())

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 } ,())

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 } ,())

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 } ,())
let z be Element of Z; :: thesis: (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,())
set L = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ;
[x,z] in [:X,Z:] ;
then A1: (R (#) S) . (x,z) = upper_bound (rng (min (R,S,x,z))) by FUZZY_4:def 3;
A2: for b being Element of () 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 (); :: thesis: ( b is_>=_than { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } implies (R (#) S) . (x,z) <<= b )
assume A3: b is_>=_than { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; :: thesis: (R (#) S) . (x,z) <<= b
A4: rng (min (R,S,x,z)) c= [.0,1.] by RELAT_1:def 19;
A5: { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } = rng (min (R,S,x,z)) by Lm4;
A6: for r being Real st r in rng (min (R,S,x,z)) holds
r <= b
proof
let r be Real; :: thesis: ( r in rng (min (R,S,x,z)) implies r <= b )
assume A7: r in rng (min (R,S,x,z)) ; :: thesis: r <= b
then reconsider r = r as Element of () by ;
r <<= b by A3, A5, A7;
hence r <= b by Th3; :: thesis: verum
end;
rng (min (R,S,x,z)) <> {} by Lm4;
then upper_bound (rng (min (R,S,x,z))) <= b by ;
hence (R (#) S) . (x,z) <<= b by ; :: thesis: verum
end;
for b being Element of () 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 (); :: 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
A8: b = (R . (x,y)) "/\" (S . (y,z)) ;
reconsider b = b as Real ;
( dom (min (R,S,x,z)) = Y & b = (min (R,S,x,z)) . y ) by ;
then b <= upper_bound (rng (min (R,S,x,z))) by FUZZY_4:1;
hence (R (#) S) . [x,z] >>= b by ; :: thesis: verum
end;
then (R (#) S) . [x,z] is_>=_than { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ;
hence (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,()) by ; :: thesis: verum