set H = ProjGroup (F,i);
set G = product F;
LM1: for a being Element of (product F) holds (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i))

proof

let a be Element of (product F); :: thesis: (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i))

now

let x be set ; :: thesis: ( x in (a * (ProjGroup (F,i))) * (a ") implies x in the carrier of (ProjGroup (F,i)) )
assume x in (a * (ProjGroup (F,i))) * (a ") ; :: thesis: x in the carrier of (ProjGroup (F,i))
then consider h being Element of (product F) such that
A1: ( x = h * (a ") & h in a * (ProjGroup (F,i)) ) by GROUP_2:34;
consider k being Element of (product F) such that
A2: ( h = a * k & k in ProjGroup (F,i) ) by GROUP_2:125, A1;
k in the carrier of (ProjGroup (F,i)) by A2, STRUCT_0:def 5;
then k in ProjSet (F,i) by defPrjGroup;
then consider m being Function, g being Element of (F . i) such that
X0: ( m = k & dom m = I & m . i = g & ( for j being Element of I st j <> i holds
m . j = 1_ (F . j) ) ) by LMP1;
set n = (a * k) * (a ");
W0: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
Y0: dom (Carrier F) = I by PARTFUN1:def 4;
X1: dom ((a * k) * (a ")) = I by PARTFUN1:def 4, W0;
set Gi = F . i;
consider Ri being 1-sorted such that
B3: ( Ri = F . i & (Carrier F) . i = the carrier of Ri ) by PRALG_1:def 13;
set ak = a * k;
set ad = a " ;
reconsider xa = a . i, xk = k . i as Element of (F . i) by B3, CARD_3:18, W0, Y0;
X10: (a * k) . i = xa * xk by GROUP_7:4;
X11: (a ") . i = xa " by GROUP_7:11;
X2: ((a * k) * (a ")) . i = (xa * xk) * (xa ") by X10, X11, GROUP_7:4;

now

let j be Element of I; :: thesis: ( j <> i implies ((a * k) * (a ")) . j = 1_ (F . j) )
assume j <> i ; :: thesis: ((a * k) * (a ")) . j = 1_ (F . j)
then X4: m . j = 1_ (F . j) by X0;
set Gj = F . j;
consider Rj being 1-sorted such that
B3: ( Rj = F . j & (Carrier F) . j = the carrier of Rj ) by PRALG_1:def 13;
reconsider xa = a . j, xk = k . j as Element of (F . j) by B3, CARD_3:18, W0, Y0;
X10: (a * k) . j = xa * xk by GROUP_7:4;
X11: (a ") . j = xa " by GROUP_7:11;
thus ((a * k) * (a ")) . j = (xa * xk) * (xa ") by X10, X11, GROUP_7:4
.= xa * (xa ") by GROUP_1:def 5, X4, X0
.= 1_ (F . j) by GROUP_1:def 6 ; :: thesis: verum

end;

then (a * k) * (a ") in ProjSet (F,i) by X1, X2, LMP1;
hence x in the carrier of (ProjGroup (F,i)) by defPrjGroup, A1, A2; :: thesis: verum

end;

hence (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) by TARSKI:def 3; :: thesis: verum

end;

LM2: for a being Element of (product F) holds a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a

proof

let a be Element of (product F); :: thesis: a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a
P1: (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) by LM1;
P2: (a ") * a = 1_ (product F) by GROUP_1:def 6;
((a * (ProjGroup (F,i))) * (a ")) * a = (a * ((ProjGroup (F,i)) * (a "))) * a by GROUP_2:128
.= a * (((ProjGroup (F,i)) * (a ")) * a) by GROUP_2:39
.= a * ((ProjGroup (F,i)) * ((a ") * a)) by GROUP_2:129
.= a * (ProjGroup (F,i)) by P2, GROUP_2:132 ;
hence a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by P1, GROUP_3:5; :: thesis: verum

end;

LM3: for a being Element of (product F) holds (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))

proof

let a be Element of (product F); :: thesis: (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))
P1: ((a ") * (ProjGroup (F,i))) * ((a ") ") c= the carrier of (ProjGroup (F,i)) by LM1;
P2: a * (a ") = 1_ (product F) by GROUP_1:def 6;
a * (((a ") * (ProjGroup (F,i))) * a) = a * ((a ") * ((ProjGroup (F,i)) * a)) by GROUP_2:128
.= (a * (a ")) * ((ProjGroup (F,i)) * a) by GROUP_2:38
.= ((a * (a ")) * (ProjGroup (F,i))) * a by GROUP_2:128
.= (ProjGroup (F,i)) * a by P2, GROUP_2:132 ;
hence (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by P1, GROUP_3:5; :: thesis: verum

end;

for a being Element of (product F) holds a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a

proof

let a be Element of (product F); :: thesis: a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a
P1: a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by LM2;
(ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by LM3;
hence a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a by P1, XBOOLE_0:def 10; :: thesis: verum

end;

hence ProjGroup (F,i) is normal by GROUP_3:140; :: thesis: verum