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