theorem Th2: :: VECTSP11:2

for n being Nat
for K being Field
for P being finite without_zero Subset of NAT st P c= Seg n holds
Segm ((1. (K,n)),P,P) = 1. (K,(card P))