theorem Th10: :: HEYTING3:10

for V, V9, C, C9 being set
for A being Element of Fin (PFuncs (V,C))
for B being Element of Fin (PFuncs (V9,C9)) st V c= V9 & C c= C9 & A = B holds
mi A = mi B