for E being non empty set
for x, y being Variable
for f being Function of VAR,E holds
( f . x = f . y iff f in St ((x '=' y),E) )