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 ;
then A2: x 'in' y = (Var1 (x 'in' y)) 'in' (Var2 (x 'in' y)) by ZF_LANG:37;
then A3: x = Var1 (x 'in' y) by ZF_LANG:2;
A4: y = Var2 (x 'in' y) by A2, ZF_LANG:2;
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 FUNCT_2:8;
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:2;
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