let x be Element of (SORTS F) . s; :: thesis: ( x is Function-like & x is Relation-like )
x is Element of product (Carrier (F,s)) by PRALG_2:def 10;
hence ( x is Function-like & x is Relation-like ) ; :: thesis: verum