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 object ; :: 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