let B, A be Category; :: thesis: for F being Functor of A,B
for f being Morphism of A st f is invertible holds
F . f is invertible
let F be Functor of A,B; :: thesis: for f being Morphism of A st f is invertible holds
F . f is invertible
let f be Morphism of A; :: thesis: ( f is invertible implies F . f is invertible )
given g being Morphism of A such that A1: dom g = cod f and
A2: cod g = dom f and
A3: f * g = id (cod f) and
A4: g * f = id (dom f) ; :: according to CAT_1:def 9 :: thesis: F . f is invertible
take F . g ; :: according to CAT_1:def 9 :: thesis: ( dom (F . g) = cod (F . f) & cod (F . g) = dom (F . f) & (F . f) * (F . g) = id (cod (F . f)) & (F . g) * (F . f) = id (dom (F . f)) )
thus ( dom (F . g) = cod (F . f) & cod (F . g) = dom (F . f) ) by A1, A2, CAT_1:64; :: thesis: ( (F . f) * (F . g) = id (cod (F . f)) & (F . g) * (F . f) = id (dom (F . f)) )
thus (F . f) * (F . g) = F . (f * g) by A2, CAT_1:64
.= id (cod (F . f)) by A3, CAT_1:63 ; :: thesis: (F . g) * (F . f) = id (dom (F . f))
thus (F . g) * (F . f) = F . (g * f) by A1, CAT_1:64
.= id (dom (F . f)) by A4, CAT_1:63 ; :: thesis: verum