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
B1: g1 = (1_ (product F)) +* (i,z1) by defPrj, A1;
consider z2 being Element of (F . i) such that
B2: g2 = (1_ (product F)) +* (i,z2) by defPrj, A1;
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2)) by LMPX2, B1, B2;
hence g1 * g2 in ProjSet (F,i) by defPrj; :: thesis: verum