set H = ProjGroup (F,i);
set G = product F;
A1: for a being Element of () holds (a * (ProjGroup (F,i))) * (a ") c= the carrier of (ProjGroup (F,i))
proof
let a be Element of (); :: 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 () such that
A2: ( x = h * (a ") & h in a * (ProjGroup (F,i)) ) by GROUP_2:28;
consider k being Element of () such that
A3: ( h = a * k & k in ProjGroup (F,i) ) by ;
k in the carrier of (ProjGroup (F,i)) by ;
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 () by GROUP_7:def 2;
A6: dom () = I by PARTFUN1:def 2;
A7: dom ((a * k) * (a ")) = I by ;
set Gi = F . i;
consider Ri being 1-sorted such that
A8: ( Ri = F . i & () . 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 ;
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 ;
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 & () . j = the carrier of Rj ) by PRALG_1:def 13;
reconsider xa = a . j, xk = k . j as Element of (F . j) by ;
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
.= xa * (xa ") by
.= 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 () holds a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a
proof
let a be Element of (); :: 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_ () 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 ;
hence a * (ProjGroup (F,i)) c= (ProjGroup (F,i)) * a by ; :: thesis: verum
end;
A19: for a being Element of () holds (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i))
proof
let a be Element of (); :: 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_ () 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 ;
hence (ProjGroup (F,i)) * a c= a * (ProjGroup (F,i)) by ; :: thesis: verum
end;
for a being Element of () holds a * (ProjGroup (F,i)) = (ProjGroup (F,i)) * a
proof
let a be Element of (); :: 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 ; :: thesis: verum
end;
hence ProjGroup (F,i) is normal by GROUP_3:117; :: thesis: verum