let E be non empty set ; :: thesis: 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
let f be Function of VAR,E; :: thesis: 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
let v1 be Element of VAR ; :: thesis: for H being ZF-formula st v1 in Free H holds
((f * decode) | (code (Free H))) . (x". v1) = f . v1
let H be ZF-formula; :: thesis: ( v1 in Free H implies ((f * decode) | (code (Free H))) . (x". v1) = f . v1 )
assume v1 in Free H ; :: thesis: ((f * decode) | (code (Free H))) . (x". v1) = f . v1
then A1: x". v1 in code (Free H) by Lm5;
dom ((f * decode) | (code (Free H))) = code (Free H) by Lm3;
hence ((f * decode) | (code (Free H))) . (x". v1) = (f * decode) . (x". v1) by A1, FUNCT_1:47
.= f . v1 by Lm4 ;
:: thesis: verum