let G be finite addGroup; :: thesis: for I, H being Subgroup of G
for J being Subgroup of H st I = J holds
index I = (index J) * (index H)
let I, H be Subgroup of G; :: thesis: for J being Subgroup of H st I = J holds
index I = (index J) * (index H)
let J be Subgroup of H; :: thesis: ( I = J implies index I = (index J) * (index H) )
assume A1: I = J ; :: thesis: index I = (index J) * (index H)
( card G = (card H) * (index H) & card H = (card J) * (index J) ) by Th147;
then (card I) * ((index J) * (index H)) = (card I) * (index I) by A1, Th147;
hence index I = (index J) * (index H) by XCMPLX_1:5; :: thesis: verum