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])
;
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, LFUZZY_0:3;
:: 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 RELAT_1:def 19, FUNCT_2:def 1, 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;
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, LFUZZY_0:def 3;
r <<= b
by A5, A7, A9, LATTICE3:def 9;
hence
r <= b
by LFUZZY_0:3;
:: thesis: verum
end;
then
upper_bound (rng (min R,S,x,z)) <= b
by TOPMETR3:1;
hence
(R (#) S) . [x,z] <<= b
by A1, LFUZZY_0:3;
:: 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