theorem Th5: :: FRAENKEL:5

for B being non empty set
for A, X being set
for phi being Element of Funcs (A,B) holds phi | X = phi | (A /\ X)