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 ;
then A2: x '=' y = (Var1 (x '=' y)) '=' (Var2 (x '=' y)) by ZF_LANG:36;
then A3: x = Var1 (x '=' y) by ZF_LANG:1;
A4: y = Var2 (x '=' y) by A2, ZF_LANG:1;
A5: 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

reconsider v = f as Element of VAL E by FUNCT_2:8;
assume f . x = f . y ; :: thesis: f in St ((x '=' y),E)
then for f being Function of VAR,E st f = v holds
f . (Var1 (x '=' y)) = f . (Var2 (x '=' y)) by A2, A3, ZF_LANG:1;
hence f in St ((x '=' y),E) by A5; :: 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 A5;
hence f . x = f . y by A3, A4; :: thesis: verum