theorem Th2: :: HEYTING2:2

for V, C being set
for a being finite Element of PFuncs (V,C) holds {a} in SubstitutionSet (V,C)