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

proof

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

end;

assume f in St (x 'in' y),E ; :: thesis: f . x in 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 'in' y)) in f . (Var2 (x 'in' y)) ) ) by A5;
hence f . x in f . y by A3, A4; :: thesis: verum