let f, g, F be Function; :: thesis: for x being set st x in dom (F * <:f,g:>) holds
(F * <:f,g:>) . x = F . (f . x),(g . x)
let x be set ; :: thesis: ( x in dom (F * <:f,g:>) implies (F * <:f,g:>) . x = F . (f . x),(g . x) )
assume A1: x in dom (F * <:f,g:>) ; :: thesis: (F * <:f,g:>) . x = F . (f . x),(g . x)
then A2: x in dom <:f,g:> by FUNCT_1:21;
thus (F * <:f,g:>) . x = F . (<:f,g:> . x) by A1, FUNCT_1:22
.= F . (f . x),(g . x) by A2, FUNCT_3:def 8 ; :: thesis: verum