let A, B be non empty set ; 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; 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; 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; (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; verum