for i being Element of I holds ((Omega). F) . i is normal Subgroup of F . i

proof

let i be Element of I; :: thesis: ((Omega). F) . i is normal Subgroup of F . i
((Omega). F) . i = (Omega). (F . i) by Def6;
hence ((Omega). F) . i is normal Subgroup of F . i ; :: thesis: verum

end;

hence (Omega). F is normal ; :: thesis: verum