let n be Nat; :: thesis:
assume A1: for k being Nat st k < n holds
for x being Variable
for E being non empty set
for H being ZF-formula
for f being Function of VAR ,E st len H = k & not x in Free H & E,f |= H holds
E,f |= All x,H ; :: thesis:
let x be Variable; :: thesis:
let E be non empty set ; :: thesis:
let H be ZF-formula; :: thesis:
let f be Function of VAR ,E; :: thesis:
assume that
A2: len H = n and
A3: ( not x in Free H & E,f |= H ) ; :: thesis:

A4: now

assume H is being_equality ; :: thesis:
then A5: ( H = (Var1 H) '=' (Var2 H) & Free H = {(Var1 H),(Var2 H)} ) by ZF_LANG:53, ZF_MODEL:1;
then A6: ( f . (Var1 H) = f . (Var2 H) & x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def 2, ZF_MODEL:12;

let g be Function of VAR ,E; :: thesis:
assume for y being Variable st g . y <> f . y holds
x = y ; :: thesis:
then ( g . (Var1 H) = f . (Var1 H) & g . (Var2 H) = f . (Var2 H) ) by A6;
hence E,g |= H by A5, A6, ZF_MODEL:12; :: thesis:

end;

hence E,f |= All x,H by ZF_MODEL:16; :: thesis:

end;

A7: now

assume H is being_membership ; :: thesis:
then A8: ( H = (Var1 H) 'in' (Var2 H) & Free H = {(Var1 H),(Var2 H)} ) by ZF_LANG:54, ZF_MODEL:1;
then A9: ( f . (Var1 H) in f . (Var2 H) & x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def 2, ZF_MODEL:13;

let g be Function of VAR ,E; :: thesis:
assume for y being Variable st g . y <> f . y holds
x = y ; :: thesis:
then ( g . (Var1 H) = f . (Var1 H) & g . (Var2 H) = f . (Var2 H) ) by A9;
hence E,g |= H by A8, A9, ZF_MODEL:13; :: thesis:

end;

hence E,f |= All x,H by ZF_MODEL:16; :: thesis:

end;

A10: now

assume A11: H is negative ; :: thesis:
then A12: ( H = 'not' (the_argument_of H) & Free H = Free (the_argument_of H) ) by ZF_LANG:def 30, ZF_MODEL:1;
assume not E,f |= All x,H ; :: thesis:
then consider g being Function of VAR ,E such that
A13: for y being Variable st g . y <> f . y holds
x = y and
A14: not E,g |= H by ZF_MODEL:16;
A15: E,g |= the_argument_of H by A12, A14, ZF_MODEL:14;
the_argument_of H is_immediate_constituent_of H by A12, ZF_LANG:def 39;
then ( len (the_argument_of H) < len H & not x in Free (the_argument_of H) ) by A3, A11, ZF_LANG:81, ZF_MODEL:1;
then E,g |= All x,(the_argument_of H) by A1, A2, A15;
then ( E,f |= the_argument_of H & not E,f |= the_argument_of H ) by A3, A12, A13, ZF_MODEL:14, ZF_MODEL:16;
hence contradiction ; :: thesis:

end;

A16: now

let g be Function of VAR ,E; :: thesis:
assume for y being Variable st g . y <> f . y holds
x = y ; :: thesis:
then ( E,g |= the_left_argument_of H & E,g |= the_right_argument_of H ) by A19, ZF_MODEL:16;
hence E,g |= H by A17, ZF_MODEL:15; :: thesis:

end;

hence E,f |= All x,H by ZF_MODEL:16; :: thesis:

end;

now

assume A20: H is universal ; :: thesis:
then A21: ( H = All (bound_in H),(the_scope_of H) & Free H = (Free (the_scope_of H)) \ {(bound_in H)} ) by ZF_LANG:62, ZF_MODEL:1;

A22: now

assume A23: x = bound_in H ; :: thesis:

let g be Function of VAR ,E; :: thesis:
assume for y being Variable holds
( not g . y <> f . y or x = y or bound_in H = y ) ; :: thesis:
then for y being Variable st g . y <> f . y holds
bound_in H = y by A23;
hence E,g |= the_scope_of H by A3, A21, ZF_MODEL:16; :: thesis:

end;

then E,f |= All x,(bound_in H),(the_scope_of H) by ZF_MODEL:22;
hence E,f |= All x,H by A20, ZF_LANG:62; :: thesis:

end;

A24: ( not x in Free (the_scope_of H) or x in {(bound_in H)} ) by A3, A21, XBOOLE_0:def 5;

assume A25: x <> bound_in H ; :: thesis:
assume not E,f |= All x,H ; :: thesis:
then consider g being Function of VAR ,E such that
A26: for y being Variable st g . y <> f . y holds
x = y and
A27: not E,g |= H by ZF_MODEL:16;
consider h being Function of VAR ,E such that
A28: for y being Variable st h . y <> g . y holds
bound_in H = y and
A29: not E,h |= the_scope_of H by A21, A27, ZF_MODEL:16;
set m = f +* (bound_in H),(h . (bound_in H));
A30: ( (f +* (bound_in H),(h . (bound_in H))) . (bound_in H) = h . (bound_in H) & ( for x being Variable st x <> bound_in H holds
(f +* (bound_in H),(h . (bound_in H))) . x = f . x ) ) by FUNCT_7:34, FUNCT_7:130;
( ( for y being Variable st (f +* (bound_in H),(h . (bound_in H))) . y <> f . y holds
bound_in H = y ) & the_scope_of H is_immediate_constituent_of H ) by A21, A30, ZF_LANG:def 39;
then ( len (the_scope_of H) < len H & E,f +* (bound_in H),(h . (bound_in H)) |= the_scope_of H ) by A3, A21, ZF_LANG:81, ZF_MODEL:16;
then A31: E,f +* (bound_in H),(h . (bound_in H)) |= All x,(the_scope_of H) by A1, A2, A24, A25, TARSKI:def 1;

let y be Variable; :: thesis:
assume A32: h . y <> (f +* (bound_in H),(h . (bound_in H))) . y ; :: thesis:
then A33: y <> bound_in H by A30;
assume x <> y ; :: thesis:
then ( f . y = g . y & (f +* (bound_in H),(h . (bound_in H))) . y = f . y & h . y = g . y ) by A26, A28, A30, A33;
hence contradiction by A32; :: thesis:

end;

hence contradiction by A29, A31, ZF_MODEL:16; :: thesis:

end;

hence E,f |= All x,H by A22; :: thesis:

end;

hence E,f |= All x,H by A4, A7, A10, A16, ZF_LANG:25; :: thesis: