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 ;
TARSKI:def 3 ( 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)) }
;
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:]
;
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; verum