theorem :: ZF_FUND1:35

for E being non empty set
for f being Function of VAR,E
for v1 being Element of VAR
for H being ZF-formula st v1 in Free H holds
((f * decode) | (code (Free H))) . (x". v1) = f . v1 by Lm9;