let A, B be category; :: thesis: for F being contravariant Functor of A,B

for o1, o2 being Object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o2,F . o1 are_iso holds

o1,o2 are_iso

let F be contravariant Functor of A,B; :: thesis: for o1, o2 being Object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o2,F . o1 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 . o2,F . o1 are_iso implies o1,o2 are_iso )

assume that

A1: ( F is full & F is faithful ) and

A2: <^o1,o2^> <> {} and

A3: <^o2,o1^> <> {} and

A4: F . o2,F . o1 are_iso ; :: thesis: o1,o2 are_iso

consider Fa being Morphism of (F . o2),(F . o1) such that

A5: Fa is iso by A4;

consider a being Morphism of o1,o2 such that

A6: Fa = F . a by A1, A2, Th17;

thus ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A2, A3; :: according to ALTCAT_3:def 6 :: thesis: ex b_{1} being M3(<^o1,o2^>) st b_{1} is iso

take a ; :: thesis: a is iso

thus a is iso by A1, A2, A3, A5, A6, Th32; :: thesis: verum

for o1, o2 being Object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o2,F . o1 are_iso holds

o1,o2 are_iso

let F be contravariant Functor of A,B; :: thesis: for o1, o2 being Object of A st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . o2,F . o1 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 . o2,F . o1 are_iso implies o1,o2 are_iso )

assume that

A1: ( F is full & F is faithful ) and

A2: <^o1,o2^> <> {} and

A3: <^o2,o1^> <> {} and

A4: F . o2,F . o1 are_iso ; :: thesis: o1,o2 are_iso

consider Fa being Morphism of (F . o2),(F . o1) such that

A5: Fa is iso by A4;

consider a being Morphism of o1,o2 such that

A6: Fa = F . a by A1, A2, Th17;

thus ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A2, A3; :: according to ALTCAT_3:def 6 :: thesis: ex b

take a ; :: thesis: a is iso

thus a is iso by A1, A2, A3, A5, A6, Th32; :: thesis: verum