A1: the carrier of (sum F) c= the carrier of (product F) by GROUP_2:def 5;
the multF of (sum F) . f,g in the carrier of (sum F) ;
then reconsider h = the multF of (sum F) . f,g as Element of product (Carrier F) by A1, Def2;
h is Function ;
hence ( the multF of (sum F) . f,g is Function-like & the multF of (sum F) . f,g is Relation-like ) ; :: thesis: verum