let I be non empty set ; :: thesis: for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of () st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)

let F be Group-like associative multMagma-Family of I; :: thesis: for i being Element of I
for g1, g2 being Element of () st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)

let i be Element of I; :: thesis: for g1, g2 being Element of () st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)

let g1, g2 be Element of (); :: thesis: ( g1 in ProjSet (F,i) & g2 in ProjSet (F,i) implies g1 * g2 in ProjSet (F,i) )
assume A1: ( g1 in ProjSet (F,i) & g2 in ProjSet (F,i) ) ; :: thesis: g1 * g2 in ProjSet (F,i)
consider z1 being Element of (F . i) such that
A2: g1 = (1_ ()) +* (i,z1) by ;
consider z2 being Element of (F . i) such that
A3: g2 = (1_ ()) +* (i,z2) by ;
g1 * g2 = (1_ ()) +* (i,(z1 * z2)) by Th3, A2, A3;
hence g1 * g2 in ProjSet (F,i) by Def1; :: thesis: verum