let G be Group; :: thesis: for B, A being Subgroup of G
for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)
let B, A be Subgroup of G; :: thesis: for D being Subgroup of A st D = A /\ B & G is finite holds
index (G,B) >= index (A,D)
let D be Subgroup of A; :: thesis: ( D = A /\ B & G is finite implies index (G,B) >= index (A,D) )
assume that
A1: D = A /\ B and
A2: G is finite ; :: thesis: index (G,B) >= index (A,D)
reconsider LCB = Left_Cosets B as non empty finite set by A2;
reconsider LCD = Left_Cosets D as non empty finite set by A2;

A3: now :: thesis: for x, y being Element of G
for x9, y9 being Element of A st x9 = x & y9 = y holds
( x * B = y * B iff x9 * D = y9 * D )

let x, y be Element of G; :: thesis: for x9, y9 being Element of A st x9 = x & y9 = y holds
( x * B = y * B iff x9 * D = y9 * D )
let x9, y9 be Element of A; :: thesis: ( x9 = x & y9 = y implies ( x * B = y * B iff x9 * D = y9 * D ) )
assume that
A4: x9 = x and
A5: y9 = y ; :: thesis: ( x * B = y * B iff x9 * D = y9 * D )
A6: y9 " = y " by A5, GROUP_2:48;
A7: (y9 ") * x9 in A ;
( x * B = y * B iff (y ") * x in B ) by GROUP_2:114;
then ( x * B = y * B iff (y9 ") * x9 in B ) by A4, A6, GROUP_2:43;
then ( x * B = y * B iff (y9 ") * x9 in D ) by A1, A7, GROUP_2:82;
hence ( x * B = y * B iff x9 * D = y9 * D ) by GROUP_2:114; :: thesis: verum

end;

defpred S₁[ set , set ] means ex a being Element of G ex a9 being Element of A st
( a = a9 & $2 = a * B & $1 = a9 * D );
A8: for x being Element of LCD ex y being Element of LCB st S₁[x,y]

proof

let x be Element of LCD; :: thesis: ex y being Element of LCB st S₁[x,y]
x in LCD ;
then consider a9 being Element of A such that
A9: x = a9 * D by GROUP_2:def 15;
reconsider a = a9 as Element of G by GROUP_2:42;
reconsider y = a * B as Element of LCB by GROUP_2:def 15;
take y ; :: thesis: S₁[x,y]
take a ; :: thesis: ex a9 being Element of A st
( a = a9 & y = a * B & x = a9 * D )
take a9 ; :: thesis: ( a = a9 & y = a * B & x = a9 * D )
thus ( a = a9 & y = a * B & x = a9 * D ) by A9; :: thesis: verum

end;

consider F being Function of LCD,LCB such that
A10: for a being Element of LCD holds S₁[a,F . a] from FUNCT_2:sch 3(A8);
A11: dom F = LCD by FUNCT_2:def 1;
A12: rng F c= LCB by RELAT_1:def 19;
A13: index D = card LCD by GROUP_2:def 18;
A14: index B = card LCB by GROUP_2:def 18;
F is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )
assume that
A15: x1 in dom F and
A16: x2 in dom F ; :: thesis: ( not F . x1 = F . x2 or x1 = x2 )
reconsider z1 = x1, z2 = x2 as Element of LCD by A15, A16, FUNCT_2:def 1;
A17: ex a being Element of G ex a9 being Element of A st
( a = a9 & F . z1 = a * B & z1 = a9 * D ) by A10;
ex b being Element of G ex b9 being Element of A st
( b = b9 & F . z2 = b * B & z2 = b9 * D ) by A10;
hence ( not F . x1 = F . x2 or x1 = x2 ) by A3, A17; :: thesis: verum

end;

then Segm (index D) c= Segm (index B) by A11, A12, A13, A14, CARD_1:10;
hence index (G,B) >= index (A,D) by NAT_1:39; :: thesis: verum