let H be ZF-formula; :: thesis: for E being non empty set st H is being_equality holds
for f being Function of VAR,E holds
( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) )
let E be non empty set ; :: thesis: ( H is being_equality implies for f being Function of VAR,E holds
( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) ) )
assume H is being_equality ; :: thesis: for f being Function of VAR,E holds
( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) )
then H = (Var1 H) '=' (Var2 H) by ZF_LANG:36;
hence for f being Function of VAR,E holds
( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) ) by Th2; :: thesis: verum