let C be non empty AltCatStr ; :: thesis: for O, A being object of
for M being Morphism of , st O is terminal holds
M is mono
let O, A be object of ; :: thesis: for M being Morphism of , st O is terminal holds
M is mono
let M be Morphism of ,; :: thesis: ( O is terminal implies M is mono )
assume A1: O is terminal ; :: thesis: M is mono
let o be object of ; :: according to ALTCAT_3:def 7 :: thesis: ( <^o,O^> = {} or for b₁, b₂ being M2(<^o,O^>) holds
( not M * b₁ = M * b₂ or b₁ = b₂ ) )
assume A2: <^o,O^> <> {} ; :: thesis: for b₁, b₂ being M2(<^o,O^>) holds
( not M * b₁ = M * b₂ or b₁ = b₂ )
let a, b be Morphism of ,; :: thesis: ( not M * a = M * b or a = b )
assume M * a = M * b ; :: thesis: a = b
consider N being Morphism of , such that
N in <^o,O^> and
A3: for M1 being Morphism of , 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