let I be non empty set ; :: thesis: for F being Group-Family of I
for D being Subgroup-Family of F st ( for i being Element of I holds D . i = (F . i) ` ) holds
sum D is strict Subgroup of (product F) `
let F be Group-Family of I; :: thesis: for D being Subgroup-Family of F st ( for i being Element of I holds D . i = (F . i) ` ) holds
sum D is strict Subgroup of (product F) `
let D be Subgroup-Family of F; :: thesis: ( ( for i being Element of I holds D . i = (F . i) ` ) implies sum D is strict Subgroup of (product F) ` )
assume A1: for i being Element of I holds D . i = (F . i) ` ; :: thesis: sum D is strict Subgroup of (product F) `
( sum D is Subgroup of product D & product D is Subgroup of product F ) ;
then A2: sum D is Subgroup of product F ;
for g being Element of (product F) st g in sum D holds
g in (product F) `

proof

let g be Element of (product F); :: thesis: ( g in sum D implies g in (product F) ` )
assume B1: g in sum D ; :: thesis: g in (product F) `
1_ (product D) = 1_ (product F) by GROUP_2:44;
then consider J being finite Subset of I, b being ManySortedSet of J such that
B2: J = support (g,D) and
B3: g = (1_ (product F)) +* b and
for j being object
for G being Group st j in I \ J & G = D . j holds
g . j = 1_ G and
B5: for j being object st j in J holds
g . j = b . j by B1, GROUP_19:7;
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) );
C1: H₁() is finite by B1;
C2: S₁[ {} ]

proof

1_ ((product F) `) in (product F) ` ;
then 1_ (product F) in (product F) ` by GROUP_2:44;
hence S₁[ {} ] by GROUP_5:73; :: thesis: verum

end;

C3: for x, B being set st x in H₁() & B c= H₁() & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in H₁() & B c= H₁() & S₁[B] implies S₁[B \/ {x}] )
assume D1: x in H₁() ; :: thesis: ( not B c= H₁() or not S₁[B] or S₁[B \/ {x}] )
assume D2: B c= H₁() ; :: thesis: ( not S₁[B] or S₁[B \/ {x}] )
assume D3: S₁[B] ; :: thesis: S₁[B \/ {x}]

per cases ( x in B or not x in B ) ;

suppose x in B ; :: thesis: S₁[B \/ {x}]

then B \/ {x} = B by XBOOLE_1:12, ZFMISC_1:31;
hence S₁[B \/ {x}] by D3; :: thesis: verum

end;

suppose not x in B ; :: thesis: S₁[B \/ {x}]

hence S₁[B \/ {x}] by A1, B1, B2, B5, D1, D2, D3, LmHeartOf62; :: thesis: verum

end;

end;

end;

S₁[H₁()] from FINSET_1:sch 2(C1, C2, C3);
hence g in (product F) ` by B2, B3, GROUP_5:73; :: thesis: verum

end;

hence sum D is strict Subgroup of (product F) ` by A2, GROUP_2:58; :: thesis: verum