let a, b be Object of (EnsCat E); :: according to ALTCAT_5:def 1 :: thesis: <^a,b^> is functional
<^a,b^> = Funcs (a,b) by ALTCAT_1:def 14;
hence <^a,b^> is functional ; :: thesis: verum