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) holds g . i is Element of (F . i)
let i be Element of I; :: thesis: for F being Group-Family of I
for g being Element of (product F) holds g . i is Element of (F . i)
let F be Group-Family of I; :: thesis: for g being Element of (product F) holds g . i is Element of (F . i)
let g be Element of (product F); :: thesis: g . i is Element of (F . i)
( g is Function & g in product F ) ;
then g . i in F . i by GROUP_19:5;
hence g . i is Element of (F . i) ; :: thesis: verum