let I be non empty set ; :: thesis: for F being Group-Family of I
for S being componentwise_strict normal Subgroup-Family of F holds (product F) ./. (product S), product (F ./. S) are_isomorphic
let F be Group-Family of I; :: thesis: for S being componentwise_strict normal Subgroup-Family of F holds (product F) ./. (product S), product (F ./. S) are_isomorphic
let S be componentwise_strict normal Subgroup-Family of F; :: thesis: (product F) ./. (product S), product (F ./. S) are_isomorphic
deffunc H₁( Element of I) -> Element of bool [: the carrier of (F . $1), the carrier of ((F . $1) ./. (S . $1)):] = nat_hom (S . $1);
A1: for i being Element of I holds H₁(i) is Homomorphism of (F . i),((F ./. S) . i)

proof

let i be Element of I; :: thesis: H₁(i) is Homomorphism of (F . i),((F ./. S) . i)
(F ./. S) . i = (F . i) ./. (S . i) by Def8;
hence H₁(i) is Homomorphism of (F . i),((F ./. S) . i) ; :: thesis: verum

end;

consider f being Homomorphism-Family of F,F ./. S such that
A2: for i being Element of I holds f . i = H₁(i) from GROUP_23:sch 4(A1);
Ker f = S

proof

B1: ( dom (Ker f) = I & dom S = I ) by PARTFUN1:def 2;
for i being Element of I holds (Ker f) . i = S . i

proof

let i be Element of I; :: thesis: (Ker f) . i = S . i
C1: f . i = nat_hom (S . i) by A2;
S . i = Ker (nat_hom (S . i)) by GROUP_6:43
.= Ker (f . i) by C1, Def8
.= (Ker f) . i by Def16 ;
hence (Ker f) . i = S . i ; :: thesis: verum

end;

hence Ker f = S by B1; :: thesis: verum

end;

then A3: Ker (product f) = product S by Th64;
A5: Image f = F ./. S

proof

B1: ( dom (Image f) = I & dom (F ./. S) = I ) by PARTFUN1:def 2;
for i being Element of I holds (Image f) . i = (F ./. S) . i

proof

let i be Element of I; :: thesis: (Image f) . i = (F ./. S) . i
C1: f . i = nat_hom (S . i) by A2;
thus (Image f) . i = Image (f . i) by Def17
.= Image (nat_hom (S . i)) by C1, Def8
.= (F . i) ./. (S . i) by GROUP_6:48
.= (F ./. S) . i by Def8 ; :: thesis: verum

end;

hence Image f = F ./. S by B1; :: thesis: verum

end;

Image (product f) = product (Image f) by Th65
.= product (F ./. S) by A5 ;
hence (product F) ./. (product S), product (F ./. S) are_isomorphic by A3, GROUP_6:78; :: thesis: verum