theorem Th2: :: ZF_MODEL:2

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