let C be non empty with_units AltCatStr ; :: thesis: for o being object of C holds <^o,o^> <> {}
let o be object of C; :: thesis: <^o,o^> <> {}
the Comp of C is with_left_units by Def18;
then ex e being set st
( e in the Arrows of C . (o,o) & ( for o9 being Element of C
for f being set st f in the Arrows of C . (o9,o) holds
( the Comp of C . (o9,o,o)) . (e,f) = f ) ) by Def9;
hence <^o,o^> <> {} ; :: thesis: verum