ex C being strict Categorial full Category st
( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) ) by Lm1;
hence ex b₁ being Categorial Category st
( ( for a being Element of A holds (I `1) . a is Object of b<sub>1</sub> ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of b₁ ) ) ; :: thesis: verum