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)) <> {} )
set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ;
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:4;
for c being object 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 object ; :: 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:4; :: 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
y in dom (min (R,S,x,z)) and
A3: c = (min (R,S,x,z)) . y by PARTFUN1:3;
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