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 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