let A, B be category; for F being covariant Functor of A,B
for o1, o2 being Object of A
for a being Morphism of o1,o2 st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is iso holds
a is iso
let F be covariant Functor of A,B; for o1, o2 being Object of A
for a being Morphism of o1,o2 st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is iso holds
a is iso
let o1, o2 be Object of A; for a being Morphism of o1,o2 st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is iso holds
a is iso
let a be Morphism of o1,o2; ( F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is iso implies a is iso )
assume that
A1:
( F is full & F is faithful )
and
A2:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} )
and
A3:
F . a is iso
; a is iso
( <^(F . o1),(F . o2)^> <> {} & <^(F . o2),(F . o1)^> <> {} )
by A2, FUNCTOR0:def 18;
then
( F . a is retraction & F . a is coretraction )
by A3, ALTCAT_3:6;
then
( a is retraction & a is coretraction )
by A1, A2, Th26, Th27;
hence
a is iso
by A2, ALTCAT_3:6; verum