let I be set ; for C being Category
for c being Object of C
for F being Function of I, the carrier' of C holds
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
let C be Category; for c being Object of C
for F being Function of I, the carrier' of C holds
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
let c be Object of C; for F being Function of I, the carrier' of C holds
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
let F be Function of I, the carrier' of C; ( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
thus
( F is Projections_family of c,I implies F opp is Injections_family of c opp ,I )
( F opp is Injections_family of c opp ,I implies F is Projections_family of c,I )
assume A5:
cods (F opp) = I --> (c opp)
; CAT_3:def 16 F is Projections_family of c,I
hence
doms F = I --> c
by Th1; CAT_3:def 13 verum