theorem Th40: :: DICKSON:41

for n being non zero Nat
for p being RelStr-yielding ManySortedSet of Segm (n + 1)
for ns being Subset of (Segm (n + 1))
for ne being Element of Segm (n + 1) st ns = n & ne = n holds
[:(product (p | ns)),(p . ne):], product p are_isomorphic