let A, B be category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum