for y, x being Variable
for H being ZF-formula st not y in variables_in H holds
( ( x in Free H implies Free (H / x,y) = ((Free H) \ {x}) \/ {y} ) & ( not x in Free H implies Free (H / x,y) = Free H ) )

for H being ZF-formula holds variables_in H is finite

for H being ZF-formula holds
( ex i being Nat st
for j being Nat st x. j in variables_in H holds
j < i & not for x being Variable holds x in variables_in H )

for x being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x in variables_in H holds
( M,v |= H iff M,v |= All x,H )

for x being Variable
for M being non empty set
for m being Element of M
for H being ZF-formula
for v being Function of VAR ,M st not x in variables_in H holds
( M,v |= H iff M,v / x,m |= H )

for x, y, z being Variable
for M being non empty set
for m1, m2, m3 being Element of M
for v being Function of VAR ,M st x <> y & y <> z & z <> x holds
( ((v / x,m1) / y,m2) / z,m3 = ((v / z,m3) / y,m2) / x,m1 & ((v / x,m1) / y,m2) / z,m3 = ((v / y,m2) / z,m3) / x,m1 )

for x1, x2, x3, x4 being Variable
for M being non empty set
for m1, m2, m3, m4 being Element of M
for v being Function of VAR ,M st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
( (((v / x1,m1) / x2,m2) / x3,m3) / x4,m4 = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m1 & (((v / x1,m1) / x2,m2) / x3,m3) / x4,m4 = (((v / x3,m3) / x4,m4) / x1,m1) / x2,m2 & (((v / x1,m1) / x2,m2) / x3,m3) / x4,m4 = (((v / x4,m4) / x2,m2) / x3,m3) / x1,m1 )

for x1, x2, x3, x4 being Variable
for M being non empty set
for m1, m2, m, m3, m4 being Element of M
for v being Function of VAR ,M holds
( ((v / x1,m1) / x2,m2) / x1,m = (v / x2,m2) / x1,m & (((v / x1,m1) / x2,m2) / x3,m3) / x1,m = ((v / x2,m2) / x3,m3) / x1,m & ((((v / x1,m1) / x2,m2) / x3,m3) / x4,m4) / x1,m = (((v / x2,m2) / x3,m3) / x4,m4) / x1,m )

for x being Variable
for M being non empty set
for m being Element of M
for H being ZF-formula
for v being Function of VAR ,M st not x in Free H holds
( M,v |= H iff M,v / x,m |= H )

for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x. 0 in Free H & M,v |= All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0))))) holds
for m1, m2 being Element of M holds
( (def_func' H,v) . m1 = m2 iff M,(v / (x. 3),m1) / (x. 4),m2 |= H )

for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st Free H c= {(x. 3),(x. 4)} & M |= All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0))))) holds
def_func' H,v = def_func H,M

for x, y being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x in variables_in H holds
( M,v |= H / y,x iff M,v / y,(v . x) |= H )

for x, y being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x in variables_in H & M,v |= H holds
M,v / x,(v . y) |= H / y,x

for x, y being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x. 0 in Free H & M,v |= All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0))))) & not x in variables_in H & y <> x. 3 & y <> x. 4 & not y in Free H & x <> x. 0 & x <> x. 3 & x <> x. 4 holds
( not x. 0 in Free (H / y,x) & M,v / x,(v . y) |= All (x. 3),(Ex (x. 0),(All (x. 4),((H / y,x) <=> ((x. 4) '=' (x. 0))))) & def_func' H,v = def_func' (H / y,x),(v / x,(v . y)) )

for x, y being Variable
for M being non empty set
for H being ZF-formula st not x in variables_in H holds
( M |= H / y,x iff M |= H )

for M being non empty set
for i being Nat
for H1 being ZF-formula
for v1 being Function of VAR ,M st not x. 0 in Free H1 & M,v1 |= All (x. 3),(Ex (x. 0),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Nat st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 ) & not x. 0 in Free H2 & M,v2 |= All (x. 3),(Ex (x. 0),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0))))) & def_func' H1,v1 = def_func' H2,v2 )

for M being non empty set
for H1 being ZF-formula
for v1 being Function of VAR ,M st not x. 0 in Free H1 & M,v1 |= All (x. 3),(Ex (x. 0),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( (Free H1) /\ (Free H2) c= {(x. 3),(x. 4)} & not x. 0 in Free H2 & M,v2 |= All (x. 3),(Ex (x. 0),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0))))) & def_func' H1,v1 = def_func' H2,v2 )

for M being non empty set
for F, G being Function st F is_definable_in M & G is_definable_in M holds
F * G is_definable_in M

for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x. 0 in Free H holds
( M,v |= All (x. 3),(Ex (x. 0),(All (x. 4),(H <=> ((x. 4) '=' (x. 0))))) iff for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) )

for M being non empty set
for H being ZF-formula
for F, G being Function st F is_definable_in M & G is_definable_in M & Free H c= {(x. 3)} holds
for FG being Function st dom FG = M & ( for v being Function of VAR ,M holds
( ( M,v |= H implies FG . (v . (x. 3)) = F . (v . (x. 3)) ) & ( M,v |= 'not' H implies FG . (v . (x. 3)) = G . (v . (x. 3)) ) ) ) holds
FG is_definable_in M

for M being non empty set
for F, G being Function st F is_parametrically_definable_in M & G is_parametrically_definable_in M holds
G * F is_parametrically_definable_in M

for M being non empty set
for H1, H2, H being ZF-formula
for v being Function of VAR ,M st {(x. 0),(x. 1),(x. 2)} misses Free H1 & M,v |= All (x. 3),(Ex (x. 0),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0))))) & {(x. 0),(x. 1),(x. 2)} misses Free H2 & M,v |= All (x. 3),(Ex (x. 0),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0))))) & {(x. 0),(x. 1),(x. 2)} misses Free H & not x. 4 in Free H holds
for FG being Function st dom FG = M & ( for m being Element of M holds
( ( M,v / (x. 3),m |= H implies FG . m = (def_func' H1,v) . m ) & ( M,v / (x. 3),m |= 'not' H implies FG . m = (def_func' H2,v) . m ) ) ) holds
FG is_parametrically_definable_in M