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

proof

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

end;

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