let I be empty set ; :: thesis: for F being multMagma-Family of I holds product F is trivial Group
let F be multMagma-Family of I; :: thesis: product F is trivial Group
product (Carrier F) = {{}} by CARD_3:10;
then ex G being trivial strict Group st product F = G by LmTriv, GROUP_7:def 2;
hence product F is trivial Group ; :: thesis: verum