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:11;
then [x,y] in [:(dom f),(dom g):] by FUNCT_3:def 8;
then [:f,g:] . (x,y) = [(f . x),(g . y)] by FUNCT_3:65;
hence (F * (f,g)) . (x,y) = F . ((f . x),(g . y)) by A1, FUNCT_1:12; :: thesis: verum