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.]))

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 (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

(R (#) S) . [x,z] >>= b

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

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.]))

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 (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

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
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 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 Lm5;

for r being Real st r in rng (min (R,S,x,z)) holds

r <= b

hence (R (#) S) . [x,z] <<= b by A1, LFUZZY_0:3; :: thesis: verum

end;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 Lm5;

for r being Real st r in rng (min (R,S,x,z)) holds

r <= b

proof

then
upper_bound (rng (min (R,S,x,z))) <= b
by SEQ_4:144;
let r be Real; :: thesis: ( r in rng (min (R,S,x,z)) implies r <= b )

assume A6: r in rng (min (R,S,x,z)) ; :: thesis: r <= b

then reconsider r = r as Element of (RealPoset [.0,1.]) by A4, LFUZZY_0:def 3;

r <<= b by A3, A5, A6, LATTICE3:def 9;

hence r <= b by LFUZZY_0:3; :: thesis: verum

end;assume A6: r in rng (min (R,S,x,z)) ; :: thesis: r <= b

then reconsider r = r as Element of (RealPoset [.0,1.]) by A4, LFUZZY_0:def 3;

r <<= b by A3, A5, A6, LATTICE3:def 9;

hence r <= b by LFUZZY_0:3; :: thesis: verum

hence (R (#) S) . [x,z] <<= b by A1, LFUZZY_0:3; :: thesis: verum

(R (#) S) . [x,z] >>= b

proof

then
(R (#) S) . [x,z] is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum }
by LATTICE3:def 9;
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

A7: b = (R . [x,y]) "/\" (S . [y,z]) ;

( dom (min (R,S,x,z)) = Y & b = (min (R,S,x,z)) . y ) by A7, FUNCT_2:def 1, FUZZY_4:def 2;

then b <= upper_bound (rng (min (R,S,x,z))) by FUZZY_4:1;

hence (R (#) S) . [x,z] >>= b by A1, LFUZZY_0:3; :: thesis: verum

end;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

A7: b = (R . [x,y]) "/\" (S . [y,z]) ;

( dom (min (R,S,x,z)) = Y & b = (min (R,S,x,z)) . y ) by A7, FUNCT_2:def 1, FUZZY_4:def 2;

then b <= upper_bound (rng (min (R,S,x,z))) by FUZZY_4:1;

hence (R (#) S) . [x,z] >>= b by A1, LFUZZY_0:3; :: thesis: verum

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