let E be non empty set ; :: thesis: for x, y being Variable
for f being Function of VAR ,E holds
( f . x = f . y iff f in St (x '=' y),E )
let x, y be Variable; :: thesis: for f being Function of VAR ,E holds
( f . x = f . y iff f in St (x '=' y),E )
let f be Function of VAR ,E; :: thesis: ( f . x = f . y iff f in St (x '=' y),E )
A1: x '=' y is being_equality by ZF_LANG:16;
then x '=' y = (Var1 (x '=' y)) '=' (Var2 (x '=' y)) by ZF_LANG:53;
then A2: ( x = Var1 (x '=' y) & y = Var2 (x '=' y) ) by ZF_LANG:6;
A3: St (x '=' y),E = { v1 where v1 is Element of VAL E : for f being Function of VAR ,E st f = v1 holds
f . (Var1 (x '=' y)) = f . (Var2 (x '=' y)) } by A1, Lm3;
thus ( f . x = f . y implies f in St (x '=' y),E ) :: thesis: ( f in St (x '=' y),E implies f . x = f . y )

proof

assume A4: f . x = f . y ; :: thesis: f in St (x '=' y),E
reconsider v = f as Element of VAL E by Def2;
for f being Function of VAR ,E st f = v holds
f . (Var1 (x '=' y)) = f . (Var2 (x '=' y)) by A2, A4;
hence f in St (x '=' y),E by A3; :: thesis: verum

end;

assume f in St (x '=' y),E ; :: thesis: f . x = f . y
then ex v1 being Element of VAL E st
( f = v1 & ( for f being Function of VAR ,E st f = v1 holds
f . (Var1 (x '=' y)) = f . (Var2 (x '=' y)) ) ) by A3;
hence f . x = f . y by A2; :: thesis: verum