theorem Th6: :: FUNCOP_1:6

for f, g being Function
for A being set holds <:f,g:> | A = <:f,(g | A):>