let A, B be category; :: thesis: for F being covariant Functor of A,B
for o1, o2 being object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o1,F . o2 are_iso holds
o1,o2 are_iso
let F be covariant Functor of A,B; :: thesis: for o1, o2 being object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o1,F . o2 are_iso holds
o1,o2 are_iso
let o1, o2 be object of A; :: thesis: ( F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o1,F . o2 are_iso implies o1,o2 are_iso )
assume that
A1: ( F is full & F is faithful ) and
A2: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) and
A3: F . o1,F . o2 are_iso ; :: thesis: o1,o2 are_iso
thus ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A2; :: according to ALTCAT_3:def 6 :: thesis: ex b₁ being M2(<^o1,o2^>) st b₁ is iso
consider Fa being Morphism of (F . o1),(F . o2) such that
A4: Fa is iso by A3, ALTCAT_3:def 6;
consider a being Morphism of o1,o2 such that
A5: Fa = F . a by A1, A2, Th16;
take a ; :: thesis: a is iso
thus a is iso by A1, A2, A4, A5, Th28; :: thesis: verum