consider C being strict Categorial full Category such that
A1: ( ( 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;
C is TargetCat of I by A1, Def9;
hence ex b₁ being TargetCat of I st
( b₁ is full & b₁ is strict ) ; :: thesis: verum