let E be non empty set ; :: thesis: for H being ZF-formula
for f, g being Function of VAR ,E st (f * decode ) | (code (Free H)) = (g * decode ) | (code (Free H)) & f in St H,E holds
g in St H,E
let H be ZF-formula; :: thesis: for f, g being Function of VAR ,E st (f * decode ) | (code (Free H)) = (g * decode ) | (code (Free H)) & f in St H,E holds
g in St H,E
let f, g be Function of VAR ,E; :: thesis: ( (f * decode ) | (code (Free H)) = (g * decode ) | (code (Free H)) & f in St H,E implies g in St H,E )
assume that
A1: (f * decode ) | (code (Free H)) = (g * decode ) | (code (Free H)) and
A2: f in St H,E ; :: thesis: g in St H,E
A3: for v1 being Element of VAR st v1 in Free H holds
f . v1 = g . v1

proof

let v1 be Element of VAR ; :: thesis: ( v1 in Free H implies f . v1 = g . v1 )
assume A4: v1 in Free H ; :: thesis: f . v1 = g . v1
hence f . v1 = ((g * decode ) | (code (Free H))) . (x". v1) by A1, Lm9
.= g . v1 by A4, Lm9 ;
:: thesis: verum

end;

E,f |= H by A2, ZF_MODEL:def 4;
then E,g |= H by A3, ZF_LANG1:84;
hence g in St H,E by ZF_MODEL:def 4; :: thesis: verum