let f, g, F be Function; :: thesis: for x being object st x in dom (F * <:f,g:>) holds
(F * <:f,g:>) . x = F . ((f . x),(g . x))
let x be object ; :: 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:11;
thus (F * <:f,g:>) . x = F . (<:f,g:> . x) by A1, FUNCT_1:12
.= F . ((f . x),(g . x)) by A2, FUNCT_3:def 7 ; :: thesis: verum