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