let a, b be Object of AltGraph(# the carrier of C, the Arrows of C #); :: according to ALTCAT_5:def 1 :: thesis: <^a,b^> is functional
reconsider a1 = a, b1 = b as Object of C ;
<^a1,b1^> is functional by Def1;
hence <^a,b^> is functional ; :: thesis: verum