begin
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
:: deftheorem defines Double_Cosets GROUP_8:def 1 :
for G being strict Group
for H, K being strict Subgroup of G
for b4 being Subset-Family of G holds
( b4 = Double_Cosets (H,K) iff for A being Subset of G holds
( A in b4 iff ex a being Element of G st A = (H * a) * K ) );
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem