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