theorem Th6: :: FREEALG:6

for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) is free