set H = ProjGroup (F,i);
set G = product F;
A1: 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 :: thesis: for x being object st x in (a * (ProjGroup (F,i))) * (a ") holds
x in the carrier of (ProjGroup (F,i))

let x be object ; :: 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
A2: ( x = h * (a ") & h in a * (ProjGroup (F,i)) ) by GROUP_2:28;
consider k being Element of (product F) such that
A3: ( h = a * k & k in ProjGroup (F,i) ) by A2, GROUP_2:103;
k in the carrier of (ProjGroup (F,i)) by A3, STRUCT_0:def 5;
then k in ProjSet (F,i) by Def2;
then consider m being Function, g being Element of (F . i) such that
A4: ( m = k & dom m = I & m . i = g & ( for j being Element of I st j <> i holds
m . j = 1_ (F . j) ) ) by Th2;
set n = (a * k) * (a ");
A5: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
A6: dom (Carrier F) = I by PARTFUN1:def 2;
A7: dom ((a * k) * (a ")) = I by A5, PARTFUN1:def 2;
set Gi = F . i;
consider Ri being 1-sorted such that
A8: ( Ri = F . i & (Carrier F) . i = the carrier of Ri ) by PRALG_1:def 15;
set ak = a * k;
set ad = a " ;
reconsider xa = a . i, xk = k . i as Element of (F . i) by A8, A5, A6, CARD_3:9;
A9: (a * k) . i = xa * xk by GROUP_7:1;
A10: (a ") . i = xa " by GROUP_7:8;
A11: ((a * k) * (a ")) . i = (xa * xk) * (xa ") by A9, A10, GROUP_7:1;

now :: thesis: for j being Element of I st j <> i holds
((a * k) * (a ")) . j = 1_ (F . j)

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 A12: m . j = 1_ (F . j) by A4;
set Gj = F . j;
consider Rj being 1-sorted such that
A13: ( Rj = F . j & (Carrier F) . j = the carrier of Rj ) by PRALG_1:def 15;
reconsider xa = a . j, xk = k . j as Element of (F . j) by A13, A5, A6, CARD_3:9;
A14: (a * k) . j = xa * xk by GROUP_7:1;
A15: (a ") . j = xa " by GROUP_7:8;
thus ((a * k) * (a ")) . j = (xa * xk) * (xa ") by A14, A15, GROUP_7:1
.= xa * (xa ") by A12, A4, GROUP_1:def 4
.= 1_ (F . j) by GROUP_1:def 5 ; :: thesis: verum

end;

then (a * k) * (a ") in ProjSet (F,i) by A7, A11, Th2;
hence x in the carrier of (ProjGroup (F,i)) by Def2, A2, A3; :: thesis: verum

end;

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

end;

A16: 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
A17: (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i)) by A1;
A18: (a ") * a = 1_ (product F) by GROUP_1:def 5;
((a * (ProjGroup (F,i))) * (a ")) * a = (a * ((ProjGroup (F,i)) * (a "))) * a by GROUP_2:106
.= a * (((ProjGroup (F,i)) * (a ")) * a) by GROUP_2:33
.= a * ((ProjGroup (F,i)) * ((a ") * a)) by GROUP_2:107
.= a * (ProjGroup (F,i)) by A18, GROUP_2:109 ;
hence a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by A17, GROUP_3:5; :: thesis: verum

end;

A19: 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))
A20: ((a ") * (ProjGroup (F,i))) * ((a ") ") c= the carrier of (ProjGroup (F,i)) by A1;
A21: a * (a ") = 1_ (product F) by GROUP_1:def 5;
a * (((a ") * (ProjGroup (F,i))) * a) = a * ((a ") * ((ProjGroup (F,i)) * a)) by GROUP_2:106
.= (a * (a ")) * ((ProjGroup (F,i)) * a) by GROUP_2:32
.= ((a * (a ")) * (ProjGroup (F,i))) * a by GROUP_2:106
.= (ProjGroup (F,i)) * a by A21, GROUP_2:109 ;
hence (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by A20, 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
A22: a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by A16;
(ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by A19;
hence a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a by A22, XBOOLE_0:def 10; :: thesis: verum

end;

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