theorem Th31: :: CALCUL_2:31

for n being Nat
for c being set st 1 <= n holds
rng (IdFinS (c,n)) = rng <*c*>