let M be non empty set ; :: thesis:
let i be Element of NAT ; :: thesis:
let H1 be ZF-formula; :: thesis:
let v1 be Function of VAR,M; :: thesis:
defpred S₁[ ZF-formula, Nat] means for v1 being Function of VAR,M st not x. 0 in Free $1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),($1 <=> ((x. 4) '=' (x. 0)))))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < $2 & 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' ($1,v1) = def_func' (H2,v2) );
defpred S₂[ Nat] means for H being ZF-formula holds S₁[H,$1];
A1: for i being Nat st S₂[i] holds
S₂[i + 1]

let i be Nat; :: thesis:
assume A2: for H being ZF-formula holds S₁[H,i] ; :: thesis:
let H be ZF-formula; :: thesis:
let v1 be Function of VAR,M; :: thesis:
assume that
A3: not x. 0 in Free H and
A4: M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; :: thesis:
A5: ( i = 0 implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) )

assume A6: i = 0 ; :: thesis:
consider k being Element of NAT such that
A7: for j being Element of NAT st x. j in variables_in H holds
j < k by Th3;
( k > 4 or not k > 4 ) ;
then consider k1 being Element of NAT such that
A8: ( ( k > 4 & k1 = k ) or ( not k > 4 & k1 = 5 ) ) ;
take F = H / ((x. 0),(x. k1)); :: thesis:
take v1 / ((x. k1),(v1 . (x. 0))) ; :: thesis:
thus for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 :: thesis:

proof

let j be Element of NAT ; :: thesis:
assume j < i + 1 ; :: thesis:
then j <= 0 by A6, NAT_1:13;
then j = 0 ;
hence ( not x. j in variables_in F or j = 3 or j = 4 ) by A8, ZF_LANG1:76, ZF_LANG1:184; :: thesis:

end;

A9: x. k1 <> x. 0 by A8, ZF_LANG1:76;
k1 <> 3 by A8;
then A10: x. k1 <> x. 3 by ZF_LANG1:76;
A11: x. k1 <> x. 4 by A8, ZF_LANG1:76;
not x. k1 in variables_in H by A7, A8, XXREAL_0:2;
hence ( not x. 0 in Free F & M,v1 / ((x. k1),(v1 . (x. 0))) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,(v1 / ((x. k1),(v1 . (x. 0))))) ) by A3, A4, A9, A10, A11, Th14; :: thesis:

end;

A12: ( i <> 0 & i <> 3 & i <> 4 implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) )

proof

A13: x. 3 <> x. 4 by ZF_LANG1:76;
assume that
A14: i <> 0 and
A15: i <> 3 and
A16: i <> 4 ; :: thesis:
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
A17: x. 0 <> x. ii by A14, ZF_LANG1:76;
consider H1 being ZF-formula, v9 being Function of VAR,M such that
A18: for j being Element of NAT st j ((x. 4) '=' (x. 0)))))))) and
A21: def_func' (H,v1) = def_func' (H1,v9) by A2, A3, A4;
consider k being Element of NAT such that
A22: for j being Element of NAT st x. j in variables_in (All ((x. 4),(x. ii),H1)) holds
j < k by Th3;
take H2 = H1 / ((x. ii),(x. k)); :: thesis:
take v2 = v9 / ((x. k),(v9 . (x. ii))); :: thesis:
A23: variables_in (All ((x. 4),(x. ii),H1)) = (variables_in H1) \/ {(x. 4),(x. ii)} by ZF_LANG1:147;
x. ii in {(x. 4),(x. ii)} by TARSKI:def 2;
then A24: x. ii in variables_in (All ((x. 4),(x. ii),H1)) by A23, XBOOLE_0:def 3;
then A25: x. ii <> x. k by A22;
then A26: v2 / ((x. ii),(v2 . (x. k))) = (v9 / ((x. ii),(v2 . (x. k)))) / ((x. k),(v9 . (x. ii))) by FUNCT_7:33;
thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 :: thesis:

proof

x. ii in {(x. ii)} by TARSKI:def 1;
then A27: not x. ii in (variables_in H1) \ {(x. ii)} by XBOOLE_0:def 5;
A28: not x. ii in {(x. k)} by A25, TARSKI:def 1;
let j be Element of NAT ; :: thesis:
A29: variables_in H2 c= ((variables_in H1) \ {(x. ii)}) \/ {(x. k)} by ZF_LANG1:187;
assume j x. k by ZF_LANG1:76;
assume A32: x. j in variables_in H2 ; :: thesis:
then ( x. j in (variables_in H1) \ {(x. ii)} or x. j in {(x. k)} ) by A29, XBOOLE_0:def 3;
then A33: x. j in variables_in H1 by A31, TARSKI:def 1, XBOOLE_0:def 5;
( j = i or j < i ) by A30, XXREAL_0:1;
hence ( j = 3 or j = 4 ) by A18, A27, A28, A29, A32, A33, XBOOLE_0:def 3; :: thesis:

end;

now :: thesis:

let e be Element of M; :: thesis:
A58: v2 . (x. k) = v9 . (x. ii) by FUNCT_7:128;
A59: (v2 / ((x. 3),e)) . (x. k) = v2 . (x. k) by A54, FUNCT_7:32, ZF_LANG1:76;
M,v9 / ((x. 3),e) |= Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))) by A20, ZF_LANG1:71;
then consider e9 being Element of M such that
A60: M,(v9 / ((x. 3),e)) / ((x. 0),e9) |= All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
A61: (((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9)) . (x. 0) = ((v9 / ((x. 3),e)) / ((x. 0),e9)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A62: ((v9 / ((x. 3),e)) / ((x. 0),e9)) . (x. 0) = e9 by FUNCT_7:128;
(((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9)) . (x. 4) = e9 by FUNCT_7:128;
then A63: M,((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9) |= (x. 4) '=' (x. 0) by A61, A62, ZF_MODEL:12;
A64: M,((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9) |= H1 <=> ((x. 4) '=' (x. 0)) by A60, ZF_LANG1:71;
then A65: M,((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9) |= H1 by A63, ZF_MODEL:19;
A66: (v2 / ((x. 3),e)) . (x. k) = ((v2 / ((x. 3),e)) / ((x. 4),e9)) . (x. k) by A43, FUNCT_7:32;
A67: (((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) . (x. k) = ((v2 / ((x. 3),e)) / ((x. 4),e9)) . (x. k) by A45, FUNCT_7:32, ZF_LANG1:76;
A68: ((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9) = ((v9 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) by FUNCT_7:33, ZF_LANG1:76;
A69: v2 / ((x. ii),(v2 . (x. k))) = (v9 / ((x. ii),(v2 . (x. k)))) / ((x. k),(v9 . (x. ii))) by A25, FUNCT_7:33;
A70: v9 / ((x. ii),(v9 . (x. ii))) = v9 by FUNCT_7:35;
((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) = (((v9 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) / ((x. k),(v9 . (x. ii))) by A46, A55, A43, A49, A53, A13, Th7;
then A71: M,((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) |= H1 by A41, A65, A68, Th5;
(((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) / ((x. ii),(v2 . (x. k))) = (((v2 / ((x. ii),(v2 . (x. k)))) / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) by A17, A37, A36, A49, A53, A13, Th7;
then M,((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) |= H2 by A41, A71, A67, A66, A59, A69, A58, A70, Th12;
then M,(v2 / ((x. 3),e)) / ((x. 4),e9) |= H2 by A51, Th9;
then A72: (def_func' (H2,v2)) . e = e9 by A51, A57, Th10;
M,((v9 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) |= H1 by A64, A63, A68, ZF_MODEL:19;
then M,(v9 / ((x. 3),e)) / ((x. 4),e9) |= H1 by A19, Th9;
hence (def_func' (H2,v2)) . e = (def_func' (H1,v9)) . e by A19, A20, A72, Th10; :: thesis:

end;

hence def_func' (H2,v2) = def_func' (H,v1) by A21; :: thesis:

end;

now :: thesis:

assume A73: ( i = 3 or i = 4 ) ; :: thesis:
thus ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) :: thesis:

proof

consider H2 being ZF-formula, v2 being Function of VAR,M such that
A74: for j being Element of NAT st j ((x. 4) '=' (x. 0)))))))) and
A77: def_func' (H,v1) = def_func' (H2,v2) by A2, A3, A4;
take H2 ; :: thesis:
take v2 ; :: thesis:
thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 :: thesis:

proof

let j be Element of NAT ; :: thesis:
assume that
A78: j < i + 1 and
A79: x. j in variables_in H2 ; :: thesis:
j <= i by A78, NAT_1:13;
then ( j < i or j = i ) by XXREAL_0:1;
hence ( j = 3 or j = 4 ) by A73, A74, A79; :: thesis:

end;

thus ( not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) by A75, A76, A77; :: thesis:

end;

hence ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) by A12, A5; :: thesis:

end;

A80: S₂[ 0 ]

proof

let H be ZF-formula; :: thesis:
let v1 be Function of VAR,M; :: thesis:
assume that
A81: not x. 0 in Free H and
A82: M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; :: thesis:
take H ; :: thesis:
take v1 ; :: thesis:
thus ( ( for j being Element of NAT st j < 0 & x. j in variables_in H & not j = 3 holds
j = 4 ) & not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H,v1) ) by A81, A82; :: thesis:

end;

for i being Nat holds S₂[i] from NAT_1:sch 2(A80, A1);
hence ( not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j ((x. 4) '=' (x. 0)))))))) & def_func' (H1,v1) = def_func' (H2,v2) ) ) ; :: thesis: