theorem :: FUNCT_2:97

for f being Function
for A0, C being set st C c= A0 holds
f .: C = (f | A0) .: C