let A, B be non empty set ; :: thesis: for F, G being Function of B,A
for I being Indexing of F,G
for m being Element of B holds (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m)
let F, G be Function of B,A; :: thesis: for I being Indexing of F,G
for m being Element of B holds (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m)
let I be Indexing of F,G; :: thesis: for m being Element of B holds (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m)
reconsider H = I `2 as ManySortedFunctor of (I `1) * F,(I `1) * G by Def8;
let m be Element of B; :: thesis: (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m)
dom ((I `1) * F) = B by PARTFUN1:def 2;
then A1: ((I `1) * F) . m = (I `1) . (F . m) by FUNCT_1:12;
( H . m is Functor of ((I `1) * F) . m,((I `1) * G) . m & dom ((I `1) * G) = B ) by PARTFUN1:def 2;
hence (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m) by A1, FUNCT_1:12; :: thesis: verum