let C be non empty with_units AltCatStr ; for o being Object of C holds
( idm o is epi & idm o is mono )
let o be Object of C; ( idm o is epi & idm o is mono )
thus
idm o is epi
idm o is mono proof
let o1 be
Object of
C;
ALTCAT_3:def 8 ( <^o,o1^> = {} or for b1, b2 being M3(<^o,o1^>) holds
( not b1 * (idm o) = b2 * (idm o) or b1 = b2 ) )
assume A1:
<^o,o1^> <> {}
;
for b1, b2 being M3(<^o,o1^>) holds
( not b1 * (idm o) = b2 * (idm o) or b1 = b2 )
let B,
C be
Morphism of
o,
o1;
( not B * (idm o) = C * (idm o) or B = C )
assume A2:
B * (idm o) = C * (idm o)
;
B = C
thus B =
B * (idm o)
by A1, ALTCAT_1:def 17
.=
C
by A1, A2, ALTCAT_1:def 17
;
verum
end;
let o1 be Object of C; ALTCAT_3:def 7 ( <^o1,o^> = {} or for b1, b2 being M3(<^o1,o^>) holds
( not (idm o) * b1 = (idm o) * b2 or b1 = b2 ) )
assume A3:
<^o1,o^> <> {}
; for b1, b2 being M3(<^o1,o^>) holds
( not (idm o) * b1 = (idm o) * b2 or b1 = b2 )
let B, C be Morphism of o1,o; ( not (idm o) * B = (idm o) * C or B = C )
assume A4:
(idm o) * B = (idm o) * C
; B = C
thus B =
(idm o) * B
by A3, ALTCAT_1:20
.=
C
by A3, A4, ALTCAT_1:20
; verum