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 A1: v1 in Free H ; :: thesis: ((f * decode ) | (code (Free H))) . (x". v1) = f . v1
A2: dom ((f * decode ) | (code (Free H))) = code (Free H) by Lm3;
x". v1 in code (Free H) by A1, Lm5;
hence ((f * decode ) | (code (Free H))) . (x". v1) = (f * decode ) . (x". v1) by A2, FUNCT_1:70
.= f . v1 by Lm4 ;
:: thesis: verum