A1: the multF of (sum F) . (f,g) in the carrier of (sum F) ;
the carrier of (sum F) c= the carrier of (product F) by GROUP_2:def 5;
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