defpred S₁[ set ] means $1 is Subset of (VAL E);
deffunc H₇( ZF-formula) -> set = St ($1,E);
deffunc H₈( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = $2 & f = v5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
$1 = y ) holds
g in X ) ) } ;
deffunc H₉( set , set ) -> set = $1 /\ $2;
deffunc H₁₀( set ) -> Element of K27((VAL E)) = (VAL E) \ $1;
deffunc H₁₁( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds
f . $1 in f . $2 } ;
deffunc H₁₂( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds
f . $1 = f . $2 } ;
A1: for b being set st S₁[b] holds
S₁[H₁₀(b)] ;
A2: for X, Y being set st S₁[X] & S₁[Y] holds
S₁[H₉(X,Y)]

proof

let X, Y be set ; :: thesis: ( S₁[X] & S₁[Y] implies S₁[H₉(X,Y)] )
assume that
A3: X is Subset of (VAL E) and
Y is Subset of (VAL E) ; :: thesis: S₁[H₉(X,Y)]
reconsider X = X as Subset of (VAL E) by A3;
X /\ Y c= VAL E ;
hence S₁[H₉(X,Y)] ; :: thesis: verum

end;

now :: thesis: for x, y being Variable holds
( { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } is Subset of (VAL E) & { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } is Subset of (VAL E) )

let x, y be Variable; :: thesis: ( { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } is Subset of (VAL E) & { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } is Subset of (VAL E) )
set X1 = { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } ;
set X2 = { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } ;
{ v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } c= VAL E

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } or a in VAL E )
assume a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } ; :: thesis: a in VAL E
then ex v1 being Element of VAL E st
( a = v1 & ( for f being Function of VAR,E st f = v1 holds
f . x = f . y ) ) ;
hence a in VAL E ; :: thesis: verum

end;

hence { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } is Subset of (VAL E) ; :: thesis: { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } is Subset of (VAL E)
{ v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } c= VAL E

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } or a in VAL E )
assume a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } ; :: thesis: a in VAL E
then ex v1 being Element of VAL E st
( a = v1 & ( for f being Function of VAR,E st f = v1 holds
f . x in f . y ) ) ;
hence a in VAL E ; :: thesis: verum

end;

hence { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } is Subset of (VAL E) ; :: thesis: verum

end;

then A4: for x, y being Variable holds
( S₁[H₁₂(x,y)] & S₁[H₁₁(x,y)] ) ;
A5: for a being set
for x being Variable st S₁[a] holds
S₁[H₈(x,a)]

proof

let a be set ; :: thesis: for x being Variable st S₁[a] holds
S₁[H₈(x,a)]
let x be Variable; :: thesis: ( S₁[a] implies S₁[H₈(x,a)] )
assume a is Subset of (VAL E) ; :: thesis: S₁[H₈(x,a)]
set Y = { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } ;
{ u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } c= VAL E

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } or b in VAL E )
assume b in { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } ; :: thesis: b in VAL E
then ex v1 being Element of VAL E st
( b = v1 & ( for X being set
for f being Function of VAR,E st X = a & f = v1 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) ) ) ;
hence b in VAL E ; :: thesis: verum

end;

hence S₁[H₈(x,a)] ; :: thesis: verum

end;

A6: for H being ZF-formula
for a being set holds
( a = H₇(H) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H₁₂(x,y)] in A & [(x 'in' y),H₁₁(x,y)] in A ) ) & [H,a] in A & ( for H9 being ZF-formula
for a being set st [H9,a] in A holds
( ( H9 is being_equality implies a = H₁₂( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H₁₁( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st
( a = H₁₀(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st
( a = H₉(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st
( a = H₈( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ) by Def3;
thus S₁[H₇(H)] from ZF_MODEL:sch 4(A6, A4, A1, A2, A5); :: thesis: verum