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

A2: now

let x, y be Element of G; :: thesis: for x', y' being Element of A st x' = x & y' = y holds
( x * B = y * B iff x' * D = y' * D )
let x', y' be Element of A; :: thesis: ( x' = x & y' = y implies ( x * B = y * B iff x' * D = y' * D ) )
assume A3: ( x' = x & y' = y ) ; :: thesis: ( x * B = y * B iff x' * D = y' * D )
A4: y' " = y " by A3, GROUP_2:57;
A5: (y' " ) * x' in A by STRUCT_0:def 5;
( x * B = y * B iff (y " ) * x in B ) by GROUP_2:137;
then ( x * B = y * B iff (y' " ) * x' in B ) by A3, A4, GROUP_2:52;
then ( x * B = y * B iff (y' " ) * x' in D ) by A1, A5, GROUP_2:99;
hence ( x * B = y * B iff x' * D = y' * D ) by GROUP_2:137; :: thesis: verum

end;

defpred S₁[ set , set ] means ex a being Element of G ex a' being Element of A st
( a = a' & $2 = a * B & $1 = a' * D );
A6: 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 a' being Element of A such that
A7: x = a' * D by GROUP_2:def 15;
reconsider a = a' as Element of G by GROUP_2:51;
reconsider y = a * B as Element of LCB by GROUP_2:def 15;
take y ; :: thesis: S₁[x,y]
take a ; :: thesis: ex a' being Element of A st
( a = a' & y = a * B & x = a' * D )
take a' ; :: thesis: ( a = a' & y = a * B & x = a' * D )
thus ( a = a' & y = a * B & x = a' * D ) by A7; :: thesis: verum

end;

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

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )
assume ( x1 in dom F & x2 in dom F ) ; :: thesis: ( not F . x1 = F . x2 or x1 = x2 )
then reconsider z1 = x1, z2 = x2 as Element of LCD by FUNCT_2:def 1;
consider a being Element of G, a' being Element of A such that
A12: ( a = a' & F . z1 = a * B & z1 = a' * D ) by A8;
consider b being Element of G, b' being Element of A such that
A13: ( b = b' & F . z2 = b * B & z2 = b' * D ) by A8;
thus ( not F . x1 = F . x2 or x1 = x2 ) by A2, A12, A13; :: thesis: verum

end;

then index D c= index B by A9, A10, A11, CARD_1:26;
hence index G,B >= index A,D by NAT_1:40; :: thesis: verum