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
( rng (min R,S,x,z) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min R,S,x,z) <> {} )
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
( rng (min R,S,x,z) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min R,S,x,z) <> {} )
let S be RMembership_Func of Y,Z; :: thesis: for x being Element of X
for z being Element of Z holds
( rng (min R,S,x,z) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min R,S,x,z) <> {} )
let x be Element of X; :: thesis: for z being Element of Z holds
( rng (min R,S,x,z) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min R,S,x,z) <> {} )
let z be Element of Z; :: thesis: ( rng (min R,S,x,z) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min R,S,x,z) <> {} )
A1: ( Y = dom (min R,S,x,z) & 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, RELSET_1:11;
set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ;
for c being set holds
( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min R,S,x,z) )

proof

let c be set ; :: thesis: ( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min R,S,x,z) )

hereby :: thesis: ( c in rng (min R,S,x,z) implies c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } )

assume c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; :: thesis: c in rng (min R,S,x,z)
then consider y being Element of Y such that
A2: c = (R . [x,y]) "/\" (S . [y,z]) ;
c = (min R,S,x,z) . y by A2, FUZZY_4:def 2;
hence c in rng (min R,S,x,z) by A1, PARTFUN1:27; :: thesis: verum

end;

assume c in rng (min R,S,x,z) ; :: thesis: c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum }
then consider y being Element of Y such that
A3: ( y in dom (min R,S,x,z) & c = (min R,S,x,z) . y ) by PARTFUN1:26;
c = (R . [x,y]) "/\" (S . [y,z]) by A3, FUZZY_4:def 2;
hence c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; :: thesis: verum

end;

hence rng (min R,S,x,z) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } by TARSKI:2; :: thesis: rng (min R,S,x,z) <> {}
thus rng (min R,S,x,z) <> {} ; :: thesis: verum