let I be non empty set ; :: thesis:
let F be Group-Family of I; :: thesis:
let D be Subgroup-Family of F; :: thesis:
assume A1: for i being Element of I holds D . i = (F . i) ` ; :: thesis:
let g be Element of (product F); :: thesis:
assume A2: g in sum D ; :: thesis:
let J be finite Subset of I; :: thesis:
let b be ManySortedSet of J; :: thesis:
assume A5: for j being object st j in J holds
g . j = b . j ; :: thesis:
let x, B be set ; :: thesis:
assume A6: x in J ; :: thesis:
assume A7: B c= J ; :: thesis:
assume A8: not x in B ; :: thesis:
deffunc H₁() -> Element of bool I = support (g,D);
defpred S₁[ set ] means ex FS being FinSequence of the carrier of (product F) ex ks being FinSequence of INT st
( len FS = len ks & rng FS c= commutators (product F) & (1_ (product F)) +* (b | $1) = Product (FS |^ ks) );
given FSB being FinSequence of the carrier of (product F), ksB being FinSequence of INT such that A9: ( len FSB = len ksB & rng FSB c= commutators (product F) & (1_ (product F)) +* (b | B) = Product (FSB |^ ksB) ) ; :: thesis:
reconsider ii = x as Element of I by A6;
g in product D by A2, GROUP_2:40;
then ( g . x = g . ii & g . ii in D . ii & D . ii = (F . ii) ` ) by A1, GROUP_19:5;
then consider FSg being FinSequence of the carrier of (F . ii), ksg being FinSequence of INT such that
A10: ( len FSg = len ksg & rng FSg c= commutators (F . ii) & g . x = Product (FSg |^ ksg) ) by GROUP_5:73;
1ProdHom (F,ii) is Homomorphism of (F . ii),(product F) by GROUP_19:6;
then consider F2 being FinSequence of the carrier of (product F) such that
A11: ( len F2 = len FSg & F2 = (1ProdHom (F,ii)) * FSg & Product (F2 |^ ksg) = (1ProdHom (F,ii)) . (Product (FSg |^ ksg)) ) by ThMappingFrobProd2;
for y being object st y in rng F2 holds
y in commutators (product F)

proof

let y be object ; :: thesis:
assume y in rng F2 ; :: thesis:
then consider xx being object such that
Z1: ( xx in dom F2 & y = F2 . xx ) by FUNCT_1:def 3;
xx in dom FSg by Z1, A11, FUNCT_1:11;
then FSg . xx in rng FSg by FUNCT_1:3;
then Z2: FSg . xx in commutators (F . ii) by A10;
Z3: y = (1ProdHom (F,ii)) . (FSg . xx) by A11, Z1, FUNCT_1:12;
1ProdHom (F,ii) is Homomorphism of (F . ii),(product F) by GROUP_19:6;
hence y in commutators (product F) by Z2, Z3, ThMorphismOfCommutators; :: thesis:

end;

then A12: rng F2 c= commutators (product F) by TARSKI:def 3;
set FS = FSB ^ F2;
set ks = ksB ^ ksg;
( len (ksB ^ ksg) = (len ksB) + (len ksg) & len (FSB ^ F2) = (len FSB) + (len F2) ) by FINSEQ_1:22;
then E1: len (ksB ^ ksg) = len (FSB ^ F2) by A9, A10, A11;
E2: rng (FSB ^ F2) c= commutators (product F)

proof

set X = (rng FSB) \/ (commutators (product F));
( (rng FSB) \/ (rng F2) c= (rng FSB) \/ (commutators (product F)) & (rng FSB) \/ (commutators (product F)) c= (commutators (product F)) \/ (commutators (product F)) ) by A9, A12, XBOOLE_1:9;
then (rng FSB) \/ (rng F2) c= commutators (product F) by XBOOLE_1:1;
hence rng (FSB ^ F2) c= commutators (product F) by FINSEQ_1:31; :: thesis:

end;

A13: ( dom (Product ((FSB ^ F2) |^ (ksB ^ ksg))) = I & dom ((1_ (product F)) +* (b | (B \/ {x}))) = I )

proof

thus dom (Product ((FSB ^ F2) |^ (ksB ^ ksg))) = I by GROUP_19:3; :: thesis:
{x} c= J by A6, ZFMISC_1:31;
then Z1: B \/ {x} c= J by A7, XBOOLE_1:8;
Z2: dom b = J by PARTFUN1:def 2;
dom ((1_ (product F)) +* (b | (B \/ {x}))) = (dom (1_ (product F))) \/ (dom (b | (B \/ {x}))) by FUNCT_4:def 1
.= I \/ (dom (b | (B \/ {x}))) by GROUP_19:3
.= I \/ (B \/ {x}) by Z1, Z2, RELAT_1:62
.= I by Z1, XBOOLE_1:1, XBOOLE_1:12 ;
hence dom ((1_ (product F)) +* (b | (B \/ {x}))) = I ; :: thesis:

end;

for j being Element of I holds ((1_ (product F)) +* (b | (B \/ {x}))) . j = (Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j

proof

let j be Element of I; :: thesis:
{x} c= J by A6, ZFMISC_1:31;
then A14: B \/ {x} c= J by A7, XBOOLE_1:8;
(FSB ^ F2) |^ (ksB ^ ksg) = (FSB |^ ksB) ^ (F2 |^ ksg) by A9, A10, A11, GROUP_4:19;
then A15: Product ((FSB ^ F2) |^ (ksB ^ ksg)) = (Product (FSB |^ ksB)) * (Product (F2 |^ ksg)) by GROUP_4:5;
A16: dom (b | (B \/ {x})) = B \/ {x} by A14, PARTFUN1:def 2;
A17: ( not j in B implies (Product (FSB |^ ksB)) . j = 1_ (F . j) )

proof

assume not j in B ; :: thesis:
then not j in dom (b | B) ;
then (1_ (product F)) . j = (Product (FSB |^ ksB)) . j by A9, FUNCT_4:11;
hence (Product (FSB |^ ksB)) . j = 1_ (F . j) by GROUP_7:6; :: thesis:

end;

A18: ( not j in {x} implies (Product (F2 |^ ksg)) . j = 1_ (F . j) )

proof

assume not j in {x} ; :: thesis:
then Z1: j <> x by TARSKI:def 1;
Z2: dom (1ProdHom (F,ii)) = the carrier of (F . ii) by FUNCT_2:def 1;
(proj (F,j)) . (Product (F2 |^ ksg)) = ((proj (F,j)) * (1ProdHom (F,ii))) . (Product (FSg |^ ksg)) by Z2, A11, FUNCT_1:13
.= (1: ((F . ii),(F . j))) . (Product (FSg |^ ksg)) by Z1, Th37
.= 1_ (F . j) ;
hence (Product (F2 |^ ksg)) . j = 1_ (F . j) by Def13; :: thesis:

end;

per cases by XBOOLE_0:def 3;

suppose A19: j in B ; :: thesis:

Z1: dom b = J by PARTFUN1:def 2;
then Z2: j in dom (b | B) by A7, A19, RELAT_1:62;
dom (b | (B \/ {x})) = B \/ {x} by A14, Z1, RELAT_1:62;
then Z3: j in dom (b | (B \/ {x})) by A19, XBOOLE_0:def 3;
Z4: (proj (F,j)) . (Product ((FSB ^ F2) |^ (ksB ^ ksg))) = ((proj (F,j)) . (Product (FSB |^ ksB))) * ((proj (F,j)) . (Product (F2 |^ ksg))) by A15, GROUP_6:def 6
.= ((proj (F,j)) . (Product (FSB |^ ksB))) * (1_ (F . j)) by A8, A19, A18, Def13, TARSKI:def 1
.= (proj (F,j)) . (Product (FSB |^ ksB)) by GROUP_1:def 4
.= (Product (FSB |^ ksB)) . j by Def13
.= (b | B) . j by A9, Z2, FUNCT_4:13
.= b . j by A19, FUNCT_1:49 ;
((1_ (product F)) +* (b | (B \/ {x}))) . j = (b | (B \/ {x})) . j by Z3, FUNCT_4:13
.= b . j by Z3, FUNCT_1:49 ;
hence ((1_ (product F)) +* (b | (B \/ {x}))) . j = (Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j by Z4, Def13; :: thesis:

end;

suppose A20: j in {x} ; :: thesis:

Z1: dom (1ProdHom (F,ii)) = the carrier of (F . ii) by FUNCT_2:def 1;
j = ii by A20, TARSKI:def 1;
then (Product (F2 |^ ksg)) . j = (proj (F,ii)) . (Product (F2 |^ ksg)) by Def13
.= ((proj (F,ii)) * (1ProdHom (F,ii))) . (Product (FSg |^ ksg)) by A11, Z1, FUNCT_1:13
.= (id the carrier of (F . ii)) . (Product (FSg |^ ksg)) by Th38
.= g . j by A10, A20, TARSKI:def 1 ;
then Z5: (proj (F,j)) . (Product (F2 |^ ksg)) = g . j by Def13;
Z3: (Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j = b . j

proof

Z4: j in J by A6, A20, TARSKI:def 1;
Z6: (proj (F,j)) . (Product (FSB |^ ksB)) = 1_ (F . j) by Def13, A8, A17, A20, TARSKI:def 1;
(Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j = (proj (F,j)) . ((Product (FSB |^ ksB)) * (Product (F2 |^ ksg))) by A15, Def13
.= (1_ (F . j)) * (g /. j) by Z5, Z6, GROUP_6:def 6
.= g /. j by GROUP_1:def 4 ;
hence (Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j = b . j by A5, Z4; :: thesis:

end;

((1_ (product F)) +* (b | (B \/ {x}))) . j = b . j

proof

j in B \/ {x} by A20, XBOOLE_0:def 3;
then ( ((1_ (product F)) +* (b | (B \/ {x}))) . j = (b | (B \/ {x})) . j & (b | (B \/ {x})) . j = b . j ) by A16, FUNCT_1:49, FUNCT_4:13;
hence ((1_ (product F)) +* (b | (B \/ {x}))) . j = b . j ; :: thesis:

end;

hence ((1_ (product F)) +* (b | (B \/ {x}))) . j = (Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j by Z3; :: thesis:

end;

suppose A21: not j in B \/ {x} ; :: thesis:

then not j in dom (b | (B \/ {x})) ;
then A22: ((1_ (product F)) +* (b | (B \/ {x}))) . j = (1_ (product F)) . j by FUNCT_4:11
.= 1_ (F . j) by GROUP_7:6 ;
(Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j = 1_ (F . j)

proof

(Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j = (proj (F,j)) . ((Product (FSB |^ ksB)) * (Product (F2 |^ ksg))) by A15, Def13
.= ((proj (F,j)) . (Product (FSB |^ ksB))) * ((proj (F,j)) . (Product (F2 |^ ksg))) by GROUP_6:def 6
.= ((proj (F,j)) . (Product (FSB |^ ksB))) * ((Product (F2 |^ ksg)) /. j) by Def13
.= ((Product (FSB |^ ksB)) /. j) * ((Product (F2 |^ ksg)) /. j) by Def13
.= 1_ (F . j) by A17, A18, A21, GROUP_1:def 4, XBOOLE_0:def 3 ;
hence (Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j = 1_ (F . j) ; :: thesis:

end;

hence ((1_ (product F)) +* (b | (B \/ {x}))) . j = (Product ((FSB ^ F2) |^ (ksB ^ ksg))) . j by A22; :: thesis:

end;

then (1_ (product F)) +* (b | (B \/ {x})) = Product ((FSB ^ F2) |^ (ksB ^ ksg)) by A13;
hence S₁[B \/ {x}] by E1, E2; :: thesis: