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