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 ;
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 ;
hence c in rng (min (R,S,x,z)) by ; :: 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 ;
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)) <> {}
ex d being set st d in rng (min (R,S,x,z))
proof
set y = the Element of Y;
take (min (R,S,x,z)) . the Element of Y ; :: thesis: (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z))
thus (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z)) by ; :: thesis: verum
end;
hence rng (min (R,S,x,z)) <> {} ; :: thesis: verum