let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I
for g being Element of (product F)
for h being Element of (F . i) holds g +* (i,h) in product F
let i be Element of I; :: thesis: for F being Group-Family of I
for g being Element of (product F)
for h being Element of (F . i) holds g +* (i,h) in product F
let F be Group-Family of I; :: thesis: for g being Element of (product F)
for h being Element of (F . i) holds g +* (i,h) in product F
let g be Element of (product F); :: thesis: for h being Element of (F . i) holds g +* (i,h) in product F
let h be Element of (F . i); :: thesis: g +* (i,h) in product F
g in product F ;
hence g +* (i,h) in product F by GROUP_19:24; :: thesis: verum