let I be non empty set ; :: thesis: for F, S being Group-Family of I
for g being Element of (product F) holds
( g in product S iff for i being Element of I holds (proj (F,i)) . g in S . i )
let F, S be Group-Family of I; :: thesis: for g being Element of (product F) holds
( g in product S iff for i being Element of I holds (proj (F,i)) . g in S . i )
let g be Element of (product F); :: thesis: ( g in product S iff for i being Element of I holds (proj (F,i)) . g in S . i )

hereby :: thesis: ( ( for i being Element of I holds (proj (F,i)) . g in S . i ) implies g in product S )

assume A1: g in product S ; :: thesis: for i being Element of I holds (proj (F,i)) . g in S . i
let i be Element of I; :: thesis: (proj (F,i)) . g in S . i
g . i in S . i by A1, GROUP_19:5;
hence (proj (F,i)) . g in S . i by Def13; :: thesis: verum

end;

assume Z2: for i being Element of I holds (proj (F,i)) . g in S . i ; :: thesis: g in product S
Z3: dom g = I by GROUP_19:3;
for i being Element of I holds g . i in S . i

proof

let i be Element of I; :: thesis: g . i in S . i
(proj (F,i)) . g in S . i by Z2;
hence g . i in S . i by Def13; :: thesis: verum

end;

hence g in product S by Z3, Th47; :: thesis: verum