theorem Th1: :: HEYTING2:1

for V, C, a, b being set st b in SubstitutionSet (V,C) & a in b holds
a is finite Function