A2: { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } c= [:[:the carrier of C,the carrier of D:],the carrier' of E:]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } or x in [:[:the carrier of C,the carrier of D:],the carrier' of E:] )
assume x in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } ; :: thesis: x in [:[:the carrier of C,the carrier of D:],the carrier' of E:]
then ex c being Object of C ex d being Object of D ex f being Morphism of E st
( x = [[c,d],f] & f in Hom (F . c),(G . d) ) ;
hence x in [:[:the carrier of C,the carrier of D:],the carrier' of E:] ; :: thesis: verum

end;

[[c1,d1],f1] in { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } by A1;
hence { [[c,d],f] where c is Object of C, d is Object of D, f is Morphism of E : f in Hom (F . c),(G . d) } is non empty Subset of [:[:the carrier of C,the carrier of D:],the carrier' of E:] by A2; :: thesis: verum