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 x 'in' y = (Var1 (x 'in' y)) 'in' (Var2 (x 'in' y)) by ZF_LANG:54;
then A2: ( x = Var1 (x 'in' y) & y = Var2 (x 'in' y) ) by ZF_LANG:7;
A3: 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

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