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 and
A4: E,f |= H ; :: thesis:

A5: now :: thesis:

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

now :: thesis:

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 A7;
hence E,g |= H by A8, A9, ZF_MODEL:12; :: thesis:

end;

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

end;

A10: now :: thesis:

assume A11: H is universal ; :: thesis:
then A12: H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
Free H = (Free (the_scope_of H)) \ {(bound_in H)} by A11, ZF_MODEL:1;
then A13: ( not x in Free (the_scope_of H) or x in {(bound_in H)} ) by A3, XBOOLE_0:def 5;

A14: now :: thesis:

assume A15: x <> bound_in H ; :: thesis:
assume not E,f |= All (x,H) ; :: thesis:
then consider g being Function of VAR,E such that
A16: for y being Variable st g . y <> f . y holds
x = y and
A17: not E,g |= H by ZF_MODEL:16;
consider h being Function of VAR,E such that
A18: for y being Variable st h . y <> g . y holds
bound_in H = y and
A19: not E,h |= the_scope_of H by A12, A17, ZF_MODEL:16;
set m = f +* ((bound_in H),(h . (bound_in H)));

A20: now :: thesis:

let y be Variable; :: thesis:
assume A21: h . y <> (f +* ((bound_in H),(h . (bound_in H)))) . y ; :: thesis:
assume x <> y ; :: thesis:
then A22: f . y = g . y by A16;
A23: y <> bound_in H by A21, FUNCT_7:128;
then (f +* ((bound_in H),(h . (bound_in H)))) . y = f . y by FUNCT_7:32;
hence contradiction by A18, A21, A23, A22; :: thesis:

end;

the_scope_of H is_immediate_constituent_of H by A12;
then A24: len (the_scope_of H) < len H by ZF_LANG:60;
for y being Variable st (f +* ((bound_in H),(h . (bound_in H)))) . y <> f . y holds
bound_in H = y by FUNCT_7:32;
then E,f +* ((bound_in H),(h . (bound_in H))) |= the_scope_of H by A4, A12, ZF_MODEL:16;
then E,f +* ((bound_in H),(h . (bound_in H))) |= All (x,(the_scope_of H)) by A1, A2, A13, A15, A24, TARSKI:def 1;
hence contradiction by A19, A20, ZF_MODEL:16; :: thesis:

end;

now :: thesis:

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

now :: 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 A25;
hence E,g |= the_scope_of H by A4, A12, ZF_MODEL:16; :: thesis:

end;

then E,f |= All (x,(bound_in H),(the_scope_of H)) by ZF_MODEL:21;
hence E,f |= All (x,H) by A11, ZF_LANG:44; :: thesis:

end;

hence E,f |= All (x,H) by A14; :: thesis:

end;

A26: now :: thesis:

assume A27: H is conjunctive ; :: thesis:
then A28: H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
then the_right_argument_of H is_immediate_constituent_of H ;
then A29: len (the_right_argument_of H) < len H by ZF_LANG:60;
the_left_argument_of H is_immediate_constituent_of H by A28;
then A30: len (the_left_argument_of H) < len H by ZF_LANG:60;
A31: Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) by A27, ZF_MODEL:1;
then A32: not x in Free (the_left_argument_of H) by A3, XBOOLE_0:def 3;
A33: not x in Free (the_right_argument_of H) by A3, A31, XBOOLE_0:def 3;
E,f |= the_right_argument_of H by A4, A28, ZF_MODEL:15;
then A34: E,f |= All (x,(the_right_argument_of H)) by A1, A2, A33, A29;
E,f |= the_left_argument_of H by A4, A28, ZF_MODEL:15;
then A35: E,f |= All (x,(the_left_argument_of H)) by A1, A2, A32, A30;

now :: thesis:

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 A35, A34, ZF_MODEL:16;
hence E,g |= H by A28, ZF_MODEL:15; :: thesis:

end;

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

end;

A36: now :: thesis:

assume A37: H is being_membership ; :: thesis:
then Free H = {(Var1 H),(Var2 H)} by ZF_MODEL:1;
then A38: ( x <> Var1 H & x <> Var2 H ) by A3, TARSKI:def 2;
A39: H = (Var1 H) 'in' (Var2 H) by A37, ZF_LANG:37;
then A40: f . (Var1 H) in f . (Var2 H) by A4, ZF_MODEL:13;

now :: thesis:

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 A38;
hence E,g |= H by A39, A40, ZF_MODEL:13; :: thesis:

end;

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

end;

now :: thesis:

assume A41: H is negative ; :: thesis:
then A42: H = 'not' (the_argument_of H) by ZF_LANG:def 30;
then the_argument_of H is_immediate_constituent_of H ;
then A43: len (the_argument_of H) < len H by ZF_LANG:60;
A44: not x in Free (the_argument_of H) by A3, A41, ZF_MODEL:1;
assume not E,f |= All (x,H) ; :: thesis:
then consider g being Function of VAR,E such that
A45: for y being Variable st g . y <> f . y holds
x = y and
A46: not E,g |= H by ZF_MODEL:16;
E,g |= the_argument_of H by A42, A46, ZF_MODEL:14;
then E,g |= All (x,(the_argument_of H)) by A1, A2, A43, A44;
then E,f |= the_argument_of H by A45, ZF_MODEL:16;
hence contradiction by A4, A42, ZF_MODEL:14; :: thesis:

end;

hence E,f |= All (x,H) by A5, A36, A26, A10, ZF_LANG:9; :: thesis: