for n being Nat
for fp being FinSequence of NAT st n > 1 & len fp >= 2 & ( for d being Element of NAT st d in dom fp holds
fp . d,n are_coprime ) holds
for fr being FinSequence of NAT st len fr = len fp & ( for d being Element of NAT st d in dom fr holds
fr . d = order ((fp . d),n) ) & ( for d, e being Element of NAT st d in dom fr & e in dom fr & d <> e holds
fr . d,fr . e are_coprime ) holds
order ((Product fp),n) = Product fr