let C be category; for o1, o2, o3 being Object of C st o1,o2 are_iso & o2,o3 are_iso holds
o1,o3 are_iso
let o1, o2, o3 be Object of C; ( o1,o2 are_iso & o2,o3 are_iso implies o1,o3 are_iso )
assume that
A1:
o1,o2 are_iso
and
A2:
o2,o3 are_iso
; o1,o3 are_iso
A3:
( <^o1,o2^> <> {} & <^o2,o3^> <> {} )
by A1, A2;
consider B being Morphism of o2,o3 such that
A4:
B is iso
by A2;
consider A being Morphism of o1,o2 such that
A5:
A is iso
by A1;
( <^o2,o1^> <> {} & <^o3,o2^> <> {} )
by A1, A2;
hence A6:
( <^o1,o3^> <> {} & <^o3,o1^> <> {} )
by A3, ALTCAT_1:def 2; ALTCAT_3:def 6 ex A being Morphism of o1,o3 st A is iso
take
B * A
; B * A is iso
thus
B * A is iso
by A3, A6, A5, A4, Th7; verum