let I be set ; :: thesis: for F being multMagma-Family of I
for a being Element of (product F) holds dom a = I
let F be multMagma-Family of I; :: thesis: for a being Element of (product F) holds dom a = I
let a be Element of (product F); :: thesis: dom a = I
a in product F ;
then a in product (Carrier F) by GROUP_7:def 2;
hence dom a = I by PARTFUN1:def 2; :: thesis: verum