let A be non empty set ; :: thesis: 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); :: thesis: the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o)
<^o,o^> = {(id o)} by Def20;
hence the Comp of (DiscrCat A) . (o,o,o) = ((id o),(id o)) :-> (id o) by FUNCOP_1:def 10; :: thesis: verum