consider T being TargetCat of I;
let T1, T2 be strict TargetCat of I; :: thesis: ( ( for T being TargetCat of I holds T1 = Image (I -functor C,T) ) & ( for T being TargetCat of I holds T2 = Image (I -functor C,T) ) implies T1 = T2 )
assume that
A1: for T being TargetCat of I holds T1 = Image (I -functor C,T) and
A2: for T being TargetCat of I holds T2 = Image (I -functor C,T) ; :: thesis: T1 = T2
thus T1 = Image (I -functor C,T) by A1
.= T2 by A2 ; :: thesis: verum