let C be non empty with_units AltCatStr ; :: thesis: for o being Object of C holds
( idm o is epi & idm o is mono )
let o be Object of C; :: thesis: ( idm o is epi & idm o is mono )
thus idm o is epi :: thesis: idm o is mono

proof

let o1 be Object of C; :: according to ALTCAT_3:def 8 :: thesis: ( <^o,o1^> = {} or for b₁, b₂ being M3(<^o,o1^>) holds
( not b₁ * (idm o) = b₂ * (idm o) or b₁ = b₂ ) )
assume A1: <^o,o1^> <> {} ; :: thesis: for b₁, b₂ being M3(<^o,o1^>) holds
( not b₁ * (idm o) = b₂ * (idm o) or b₁ = b₂ )
let B, C be Morphism of o,o1; :: thesis: ( not B * (idm o) = C * (idm o) or B = C )
assume A2: B * (idm o) = C * (idm o) ; :: thesis: B = C
thus B = B * (idm o) by A1, ALTCAT_1:def 17
.= C by A1, A2, ALTCAT_1:def 17 ; :: thesis: verum

end;

let o1 be Object of C; :: according to ALTCAT_3:def 7 :: thesis: ( <^o1,o^> = {} or for b₁, b₂ being M3(<^o1,o^>) holds
( not (idm o) * b₁ = (idm o) * b₂ or b₁ = b₂ ) )
assume A3: <^o1,o^> <> {} ; :: thesis: for b₁, b₂ being M3(<^o1,o^>) holds
( not (idm o) * b₁ = (idm o) * b₂ or b₁ = b₂ )
let B, C be Morphism of o1,o; :: thesis: ( not (idm o) * B = (idm o) * C or B = C )
assume A4: (idm o) * B = (idm o) * C ; :: thesis: B = C
thus B = (idm o) * B by A3, ALTCAT_1:20
.= C by A3, A4, ALTCAT_1:20 ; :: thesis: verum