let G be Group; :: thesis: ( G is finite implies for C being Subgroup of G
for A, B being Subgroup of C st C = A "\/" B holds
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E ) )
assume A1: G is finite ; :: thesis: for C being Subgroup of G
for A, B being Subgroup of C st C = A "\/" B holds
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E )
let C be Subgroup of G; :: thesis: for A, B being Subgroup of C st C = A "\/" B holds
for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E )
let A, B be Subgroup of C; :: thesis: ( C = A "\/" B implies for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E ) )
assume A2: C = A "\/" B ; :: thesis: for D being Subgroup of A st D = A /\ B holds
for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E )
let D be Subgroup of A; :: thesis: ( D = A /\ B implies for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E ) )
assume A3: D = A /\ B ; :: thesis: for E being Subgroup of B st E = A /\ B holds
for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E )
let E be Subgroup of B; :: thesis: ( E = A /\ B implies for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E ) )
assume A4: E = A /\ B ; :: thesis: for F being Subgroup of C st F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime holds
( index C,B = index A,D & index C,A = index B,E )
let F be Subgroup of C; :: thesis: ( F = A /\ B & Left_Cosets B is finite & Left_Cosets A is finite & index C,A, index C,B are_relative_prime implies ( index C,B = index A,D & index C,A = index B,E ) )
assume A5: F = A /\ B ; :: thesis: ( not Left_Cosets B is finite or not Left_Cosets A is finite or not index C,A, index C,B are_relative_prime or ( index C,B = index A,D & index C,A = index B,E ) )
assume A6: ( Left_Cosets B is finite & Left_Cosets A is finite & index A, index B are_relative_prime ) ; :: thesis: ( index C,B = index A,D & index C,A = index B,E )
A7: ( C is finite & F = E & F = D ) by A1, A3, A4, A5;
then index F = (index E) * (index B) by GROUP_2:179;
then A8: (index E) * (index B) = (index D) * (index A) by A7, GROUP_2:179;
then index B divides (index A) * (index D) by INT_1:def 9;
then A9: index B divides index D by A6, INT_2:40;
A10: index B divides index D

proof

ex n being Element of NAT st index D = (index B) * n

proof

consider i being Integer such that
A11: index D = (index B) * i by A9, INT_1:def 9;
0 <= i by A1, A11, Th20;
then reconsider i = i as Element of NAT by INT_1:16;
take n = i; :: thesis: index D = (index B) * n
thus index D = (index B) * n by A11; :: thesis: verum

end;

hence index B divides index D by NAT_D:def 3; :: thesis: verum

end;

A13: index C,B >= index A,D by A2, A3, A7, Th19;
A14: index B = index D

proof

assume A15: index B <> index D ; :: thesis: contradiction
A is finite by A1;
then index D > 0 by Th20;
then index B <= index D by A10, NAT_D:7;
hence contradiction by A13, A15, XXREAL_0:1; :: thesis: verum

end;

index A divides (index B) * (index E) by A8, INT_1:def 9;
then A16: index A divides index E by A6, INT_2:40;
A17: index A divides index E

proof

ex n being Element of NAT st index E = (index A) * n

proof

consider i being Integer such that
A18: index E = (index A) * i by A16, INT_1:def 9;
0 <= i by A1, A18, Th20;
then reconsider i = i as Element of NAT by INT_1:16;
take n = i; :: thesis: index E = (index A) * n
thus index E = (index A) * n by A18; :: thesis: verum

end;

hence index A divides index E by NAT_D:def 3; :: thesis: verum

end;

A20: index A >= index E

proof

C = B "\/" A by A2, GROUP_4:74;
hence index A >= index E by A4, A7, Th19; :: thesis: verum

end;

index A = index E

proof

assume A21: index A <> index E ; :: thesis: contradiction
B is finite by A1;
then index E > 0 by Th20;
then index A <= index E by A17, NAT_D:7;
hence contradiction by A20, A21, XXREAL_0:1; :: thesis: verum

end;

hence ( index C,B = index A,D & index C,A = index B,E ) by A14; :: thesis: verum