theorem Th83: :: GROUP_9:83

for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for FG being FinSequence of the carrier of G
for FH being FinSequence of the carrier of H
for I being FinSequence of INT st FG = FH & len FG = len I holds
Product (FG |^ I) = Product (FH |^ I)