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 Def16;
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 ) ) ;
hence <^o,o^> <> {} ; :: thesis: verum