theorem Th41: :: DICKSON:42

for n being non zero Nat
for p being RelStr-yielding ManySortedSet of Segm n st ( for i being Element of Segm n holds
( p . i is Dickson & p . i is quasi_ordered ) ) holds
( product p is quasi_ordered & product p is Dickson )