theorem :: ZF_FUND1:32

for E being non empty set
for f being Function of VAR,E
for v1 being Element of VAR holds
( decode . (x". v1) = v1 & (decode ") . v1 = x". v1 & (f * decode) . (x". v1) = f . v1 ) by Lm4;