let G be finite Group; :: 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

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