theorem Th8: :: WAYBEL10:8

for S, T being non empty RelStr
for R being non empty SubRelStr of S
for f being Function of S,T
for g being Function of T,S st f is one-to-one & g = f " holds
( g | (Image (f | R)) is Function of (Image (f | R)),R & g | (Image (f | R)) = (f | R) " )