theorem Th6: :: GLIBPRE1:6

for f being non empty one-to-one Function
for X being non empty Subset of (bool (dom f)) holds rng ((.: f) | X) = { (f .: x) where x is Element of X : verum }