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

(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