thus for N1, N2 being componentwise_strict normal Subgroup-Family of F1 st ( for i being Element of I holds N1 . i = Ker (f . i) ) & ( for i being Element of I holds N2 . i = Ker (f . i) ) holds
N1 = N2 :: thesis: verum

proof

let N1, N2 be componentwise_strict normal Subgroup-Family of F1; :: thesis: ( ( for i being Element of I holds N1 . i = Ker (f . i) ) & ( for i being Element of I holds N2 . i = Ker (f . i) ) implies N1 = N2 )
assume A1: for i being Element of I holds N1 . i = Ker (f . i) ; :: thesis: ( ex i being Element of I st not N2 . i = Ker (f . i) or N1 = N2 )
assume A2: for i being Element of I holds N2 . i = Ker (f . i) ; :: thesis: N1 = N2
A3: ( dom N1 = I & dom N2 = I ) by PARTFUN1:def 2;
for i being Element of I holds N1 . i = N2 . i

proof

let i be Element of I; :: thesis: N1 . i = N2 . i
thus N1 . i = Ker (f . i) by A1
.= N2 . i by A2 ; :: thesis: verum

end;

hence N1 = N2 by A3; :: thesis: verum

end;