theorem Th44: :: CAT_3:44

for x1, x2 being set
for C being Category
for a being Object of C
for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds
(x1,x2) --> (p1,p2) is Projections_family of a,{x1,x2}