theorem Th30: :: VALUED_0:30

for X, Y being non empty set
for s being sequence of X
for h being PartFunc of X,Y st rng s c= dom h holds
h .: (rng s) = rng (h /* s)