theorem Th37: :: GROUP_23:40

for I being non empty set
for F being Group-Family of I
for i, j being Element of I st i <> j holds
(proj (F,j)) * (1ProdHom (F,i)) = 1: ((F . i),(F . j))