let I be non empty set ; :: thesis: for F being Group-Family of I
for i being Element of I
for g being Element of (product F) holds g +* (i,(1_ (F . i))) in Ker (proj (F,i))
let F be Group-Family of I; :: thesis: for i being Element of I
for g being Element of (product F) holds g +* (i,(1_ (F . i))) in Ker (proj (F,i))
let i be Element of I; :: thesis: for g being Element of (product F) holds g +* (i,(1_ (F . i))) in Ker (proj (F,i))
let g be Element of (product F); :: thesis: g +* (i,(1_ (F . i))) in Ker (proj (F,i))
A1: dom g = I by GROUP_19:3;
g +* (i,(1_ (F . i))) in product F by Th34;
then reconsider h = g +* (i,(1_ (F . i))) as Element of (product F) ;
(proj (F,i)) . h = h . i by Def13
.= 1_ (F . i) by A1, FUNCT_7:31 ;
hence g +* (i,(1_ (F . i))) in Ker (proj (F,i)) by GROUP_6:41; :: thesis: verum