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

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

r <= b

then upper_bound (rng (min (R,S,x,z))) <= b by A6, SEQ_4:144;

hence (R (#) S) . (x,z) <<= b by A1, Th3; :: 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 Lm4;

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

r <= b

proof

rng (min (R,S,x,z)) <> {}
by Lm4;
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 (RealPoset [.0,1.]) by A4, Def3;

r <<= b by A3, A5, A7;

hence r <= b by Th3; :: thesis: verum

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

then reconsider r = r as Element of (RealPoset [.0,1.]) by A4, Def3;

r <<= b by A3, A5, A7;

hence r <= b by Th3; :: thesis: verum

then upper_bound (rng (min (R,S,x,z))) <= b by A6, SEQ_4:144;

hence (R (#) S) . (x,z) <<= b by A1, Th3; :: 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 }
;
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

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 A8, 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, Th3; :: 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

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 A8, 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, Th3; :: 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