let x, y be set ; :: thesis: for F, f, g being Function st [x,y] in dom (F * f,g) holds
(F * f,g) . x,y = F . (f . x),(g . y)
let F, f, g be Function; :: thesis: ( [x,y] in dom (F * f,g) implies (F * f,g) . x,y = F . (f . x),(g . y) )
assume A1: [x,y] in dom (F * f,g) ; :: thesis: (F * f,g) . x,y = F . (f . x),(g . y)
[x,y] in dom [:f,g:] by A1, FUNCT_1:21;
then [x,y] in [:(dom f),(dom g):] by FUNCT_3:def 9;
then [:f,g:] . x,y = [(f . x),(g . y)] by FUNCT_3:86;
hence (F * f,g) . x,y = F . (f . x),(g . y) by A1, FUNCT_1:22; :: thesis: verum