let A be non empty set ; for o being object of (DiscrCat A) holds the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)
let o be object of (DiscrCat A); the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)
<^o,o^> = {(id o)}
by Def22;
hence
the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)
by FUNCOP_1:def 10; verum