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