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 (product F) 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 (product F) 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 (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds

g1 * g2 in ProjSet (F,i)

let g1, g2 be Element of (product F); :: 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_ (product F)) +* (i,z1) by Def1, A1;

consider z2 being Element of (F . i) such that

A3: g2 = (1_ (product F)) +* (i,z2) by Def1, A1;

g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) by Th3, A2, A3;

hence g1 * g2 in ProjSet (F,i) by Def1; :: thesis: verum

for i being Element of I

for g1, g2 being Element of (product F) 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 (product F) 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 (product F) st g1 in ProjSet (F,i) & g2 in ProjSet (F,i) holds

g1 * g2 in ProjSet (F,i)

let g1, g2 be Element of (product F); :: 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_ (product F)) +* (i,z1) by Def1, A1;

consider z2 being Element of (F . i) such that

A3: g2 = (1_ (product F)) +* (i,z2) by Def1, A1;

g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) by Th3, A2, A3;

hence g1 * g2 in ProjSet (F,i) by Def1; :: thesis: verum