set H = prod_bundle F;
A1: dom (prod_bundle F) = I by PARTFUN1:def 2;
for i being object st i in I holds
(prod_bundle F) . i is Group
proof
let i be object ; :: thesis: ( i in I implies (prod_bundle F) . i is Group )
assume i in I ; :: thesis: (prod_bundle F) . i is Group
then reconsider i = i as Element of I ;
(prod_bundle F) . i = product (F . i) by Def6;
hence (prod_bundle F) . i is Group ; :: thesis: verum
end;
hence prod_bundle F is Group-Family of I by A1, GROUP_19:2; :: thesis: verum