let C be non empty AltCatStr ; :: thesis: for O, A being Object of C
for M being Morphism of O,A st O is terminal holds
M is mono
let O, A be Object of C; :: thesis: for M being Morphism of O,A st O is terminal holds
M is mono
let M be Morphism of O,A; :: thesis: ( O is terminal implies M is mono )
assume A1: O is terminal ; :: thesis: M is mono
let o be Object of C; :: according to ALTCAT_3:def 7 :: thesis: ( <^o,O^> = {} or for b₁, b₂ being M3(<^o,O^>) holds
( not M * b₁ = M * b₂ or b₁ = b₂ ) )
assume A2: <^o,O^> <> {} ; :: thesis: for b₁, b₂ being M3(<^o,O^>) holds
( not M * b₁ = M * b₂ or b₁ = b₂ )
let a, b be Morphism of o,O; :: thesis: ( not M * a = M * b or a = b )
assume M * a = M * b ; :: thesis: a = b
consider N being Morphism of o,O such that
N in <^o,O^> and
A3: for M1 being Morphism of o,O st M1 in <^o,O^> holds
N = M1 by A1, ALTCAT_3:27;
thus a = N by A2, A3
.= b by A2, A3 ; :: thesis: verum