theorem Th5: :: FUNCOP_1:5

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