theorem :: FUNCOP_1:22

for f, g, F being Function
for x being object st x in dom (F .: (f,g)) holds
(F .: (f,g)) . x = F . ((f . x),(g . x)) by Lm1;