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