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:75;
hence g in St (H,E) by ZF_MODEL:def 4; :: thesis: verum