A2: { [[c,d],f] where c is Object of , d is Object of , f is Morphism of : 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 , d is Object of , f is Morphism of : 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 , d is Object of , f is Morphism of : 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 ex d being Object of ex f being Morphism of 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 , d is Object of , f is Morphism of : f in Hom (F . c),(G . d) } by A1;
hence { [[c,d],f] where c is Object of , d is Object of , f is Morphism of : f in Hom (F . c),(G . d) } is non empty Subset of by A2; :: thesis: verum