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 4;
then A1: ((I `1 ) * F) . m = (I `1 ) . (F . m) by FUNCT_1:22;
( H . m is Functor of ((I `1 ) * F) . m,((I `1 ) * G) . m & dom ((I `1 ) * G) = B ) by PARTFUN1:def 4;
hence (I `2 ) . m is Functor of (I `1 ) . (F . m),(I `1 ) . (G . m) by A1, FUNCT_1:22; :: thesis: verum