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))

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

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

end;now :: thesis: for x being object st x in (a * (ProjGroup (F,i))) * (a ") holds

x in the carrier of (ProjGroup (F,i))

hence
(a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i))
by TARSKI:def 3; :: thesis: verumx 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;

hence x in the carrier of (ProjGroup (F,i)) by Def2, A2, A3; :: thesis: verum

end;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)

then
(a * k) * (a ") in ProjSet (F,i)
by A7, A11, Th2;((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;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

hence x in the carrier of (ProjGroup (F,i)) by Def2, A2, A3; :: thesis: verum

proof

A19:
for a being Element of (product F) holds (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))
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;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

proof

for a being Element of (product F) holds a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a
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;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

proof

hence
ProjGroup (F,i) is normal
by GROUP_3:117; :: thesis: verum
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;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