set T = the 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, the TargetCat of I)) by A1
.= T2 by A2 ; :: thesis: verum