(SORTS AF) . s = product (Carrier (AF,s)) by PRALG_2:def 10;
hence (SORTS AF) . s is functional ; :: thesis: verum