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

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