let M be non empty set ; :: thesis: for i being Element of 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 Element of 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) )

let i be Element of NAT ; :: thesis: 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 Element of 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) )

let H1 be ZF-formula; :: thesis: 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 Element of 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) )

let v1 be Function of VAR,M; :: thesis: ( 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 < 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) ) )

defpred S_{1}[ 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_{2}[ Nat] means for H being ZF-formula holds S_{1}[H,$1];

A1: for i being Nat st S_{2}[i] holds

S_{2}[i + 1]
_{2}[ 0 ]
_{2}[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 < 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) ) ) ; :: thesis: verum

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 Element of 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) )

let i be Element of NAT ; :: thesis: 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 Element of 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) )

let H1 be ZF-formula; :: thesis: 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 Element of 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) )

let v1 be Function of VAR,M; :: thesis: ( 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 < 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) ) )

defpred S

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

A1: for i being Nat st S

S

proof

A80:
S
let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume A2: for H being ZF-formula holds S_{1}[H,i]
; :: thesis: S_{2}[i + 1]

let H be ZF-formula; :: thesis: S_{1}[H,i + 1]

let v1 be Function of VAR,M; :: thesis: ( not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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 < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )

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: ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

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 < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) by A12, A5; :: thesis: verum

end;assume A2: for H being ZF-formula holds S

let H be ZF-formula; :: thesis: S

let v1 be Function of VAR,M; :: thesis: ( not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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 < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )

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: ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

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 < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )

proof

A12:
( i <> 0 & i <> 3 & i <> 4 implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
assume A6:
i = 0
; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

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: ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds

j = 4 ) & not x. 0 in Free F & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,v2) )

take v1 / ((x. k1),(v1 . (x. 0))) ; :: thesis: ( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds

j = 4 ) & 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))))) )

thus for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds

j = 4 :: thesis: ( 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))))) )

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: verum

end;( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

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: ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds

j = 4 ) & not x. 0 in Free F & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,v2) )

take v1 / ((x. k1),(v1 . (x. 0))) ; :: thesis: ( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds

j = 4 ) & 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))))) )

thus for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds

j = 4 :: thesis: ( 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))))) )

proof

A9:
x. k1 <> x. 0
by A8, ZF_LANG1:76;
let j be Element of NAT ; :: thesis: ( j < i + 1 & x. j in variables_in F & not j = 3 implies j = 4 )

assume j < i + 1 ; :: thesis: ( not x. j in variables_in F or j = 3 or j = 4 )

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: verum

end;assume j < i + 1 ; :: thesis: ( not x. j in variables_in F or j = 3 or j = 4 )

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: verum

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: verum

( ( for j being Element of NAT st j < i + 1 & 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' (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: ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

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 < i & x. j in variables_in H1 & not j = 3 holds

j = 4 and

A19: not x. 0 in Free H1 and

A20: M,v9 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((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: ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

take v2 = v9 / ((x. k),(v9 . (x. ii))); :: thesis: ( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

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: ( 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) )

A35: Free H2 c= ((Free H1) \ {(x. ii)}) \/ {(x. k)} by Th1;

A36: x. 4 <> x. ii by A16, ZF_LANG1:76;

A37: x. 3 <> x. ii by A15, ZF_LANG1:76;

then A38: (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) / ((x. ii),(x. k)) = All ((x. 3),((Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))) / ((x. ii),(x. k)))) by ZF_LANG1:159

.= All ((x. 3),(Ex ((x. 0),((All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))) / ((x. ii),(x. k)))))) by A17, ZF_LANG1:164

.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H1 <=> ((x. 4) '=' (x. 0))) / ((x. ii),(x. k)))))))) by A36, ZF_LANG1:159

.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> (((x. 4) '=' (x. 0)) / ((x. ii),(x. k))))))))) by ZF_LANG1:163

.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) by A17, A36, ZF_LANG1:152 ;

A39: v9 / ((x. ii),(v9 . (x. ii))) = v9 by FUNCT_7:35;

A40: not x. 0 in (Free H1) \ {(x. ii)} by A19, XBOOLE_0:def 5;

not x. k in variables_in (All ((x. 4),(x. ii),H1)) by A22;

then A41: not x. k in variables_in H1 by A23, XBOOLE_0:def 3;

x. 4 in {(x. 4),(x. ii)} by TARSKI:def 2;

then A42: x. 4 in variables_in (All ((x. 4),(x. ii),H1)) by A23, XBOOLE_0:def 3;

then A43: x. 4 <> x. k by A22;

then A44: not x. k in {(x. 4)} by TARSKI:def 1;

A45: 0 <> k by A22, A42;

then A46: x. 0 <> x. k by ZF_LANG1:76;

then A47: not x. k in {(x. 0)} by TARSKI:def 1;

not x. k in {(x. 4),(x. 0)} by A46, A43, TARSKI:def 2;

then not x. k in (variables_in H1) \/ {(x. 4),(x. 0)} by A41, XBOOLE_0:def 3;

then not x. k in ((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)} by A44, XBOOLE_0:def 3;

then A48: not x. k in (((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)} by A47, XBOOLE_0:def 3;

A49: x. 0 <> x. 3 by ZF_LANG1:76;

A50: not x. 0 in {(x. k)} by A46, TARSKI:def 1;

then A51: not x. 0 in Free H2 by A40, A35, XBOOLE_0:def 3;

thus not x. 0 in Free H2 by A40, A50, A35, XBOOLE_0:def 3; :: thesis: ( M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )

A52: variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) = (variables_in (Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) \/ {(x. 3)} by ZF_LANG1:142

.= ((variables_in (All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:146

.= (((variables_in (H1 <=> ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:142

.= ((((variables_in H1) \/ (variables_in ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:145

.= ((((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:138 ;

A53: x. 0 <> x. 4 by ZF_LANG1:76;

A54: 3 <> k by A22, A42;

then A55: x. 3 <> x. k by ZF_LANG1:76;

then not x. k in {(x. 3)} by TARSKI:def 1;

then A56: not x. k in variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) by A52, A48, XBOOLE_0:def 3;

then M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) by A20, Th5;

hence A57: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) by A38, A56, A34, A39, A26, Th12; :: thesis: def_func' (H,v1) = def_func' (H2,v2)

end;assume that

A14: i <> 0 and

A15: i <> 3 and

A16: i <> 4 ; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

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 < i & x. j in variables_in H1 & not j = 3 holds

j = 4 and

A19: not x. 0 in Free H1 and

A20: M,v9 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((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: ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

take v2 = v9 / ((x. k),(v9 . (x. ii))); :: thesis: ( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

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: ( 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) )

proof

A34:
v2 . (x. k) = v9 . (x. ii)
by FUNCT_7:128;
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: ( j < i + 1 & x. j in variables_in H2 & not j = 3 implies j = 4 )

A29: variables_in H2 c= ((variables_in H1) \ {(x. ii)}) \/ {(x. k)} by ZF_LANG1:187;

assume j < i + 1 ; :: thesis: ( not x. j in variables_in H2 or j = 3 or j = 4 )

then A30: j <= i by NAT_1:13;

then j < k by A22, A24, XXREAL_0:2;

then A31: x. j <> x. k by ZF_LANG1:76;

assume A32: x. j in variables_in H2 ; :: thesis: ( j = 3 or j = 4 )

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: verum

end;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: ( j < i + 1 & x. j in variables_in H2 & not j = 3 implies j = 4 )

A29: variables_in H2 c= ((variables_in H1) \ {(x. ii)}) \/ {(x. k)} by ZF_LANG1:187;

assume j < i + 1 ; :: thesis: ( not x. j in variables_in H2 or j = 3 or j = 4 )

then A30: j <= i by NAT_1:13;

then j < k by A22, A24, XXREAL_0:2;

then A31: x. j <> x. k by ZF_LANG1:76;

assume A32: x. j in variables_in H2 ; :: thesis: ( j = 3 or j = 4 )

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: verum

A35: Free H2 c= ((Free H1) \ {(x. ii)}) \/ {(x. k)} by Th1;

A36: x. 4 <> x. ii by A16, ZF_LANG1:76;

A37: x. 3 <> x. ii by A15, ZF_LANG1:76;

then A38: (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) / ((x. ii),(x. k)) = All ((x. 3),((Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))) / ((x. ii),(x. k)))) by ZF_LANG1:159

.= All ((x. 3),(Ex ((x. 0),((All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))) / ((x. ii),(x. k)))))) by A17, ZF_LANG1:164

.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H1 <=> ((x. 4) '=' (x. 0))) / ((x. ii),(x. k)))))))) by A36, ZF_LANG1:159

.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> (((x. 4) '=' (x. 0)) / ((x. ii),(x. k))))))))) by ZF_LANG1:163

.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) by A17, A36, ZF_LANG1:152 ;

A39: v9 / ((x. ii),(v9 . (x. ii))) = v9 by FUNCT_7:35;

A40: not x. 0 in (Free H1) \ {(x. ii)} by A19, XBOOLE_0:def 5;

not x. k in variables_in (All ((x. 4),(x. ii),H1)) by A22;

then A41: not x. k in variables_in H1 by A23, XBOOLE_0:def 3;

x. 4 in {(x. 4),(x. ii)} by TARSKI:def 2;

then A42: x. 4 in variables_in (All ((x. 4),(x. ii),H1)) by A23, XBOOLE_0:def 3;

then A43: x. 4 <> x. k by A22;

then A44: not x. k in {(x. 4)} by TARSKI:def 1;

A45: 0 <> k by A22, A42;

then A46: x. 0 <> x. k by ZF_LANG1:76;

then A47: not x. k in {(x. 0)} by TARSKI:def 1;

not x. k in {(x. 4),(x. 0)} by A46, A43, TARSKI:def 2;

then not x. k in (variables_in H1) \/ {(x. 4),(x. 0)} by A41, XBOOLE_0:def 3;

then not x. k in ((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)} by A44, XBOOLE_0:def 3;

then A48: not x. k in (((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)} by A47, XBOOLE_0:def 3;

A49: x. 0 <> x. 3 by ZF_LANG1:76;

A50: not x. 0 in {(x. k)} by A46, TARSKI:def 1;

then A51: not x. 0 in Free H2 by A40, A35, XBOOLE_0:def 3;

thus not x. 0 in Free H2 by A40, A50, A35, XBOOLE_0:def 3; :: thesis: ( M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )

A52: variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) = (variables_in (Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) \/ {(x. 3)} by ZF_LANG1:142

.= ((variables_in (All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:146

.= (((variables_in (H1 <=> ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:142

.= ((((variables_in H1) \/ (variables_in ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:145

.= ((((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:138 ;

A53: x. 0 <> x. 4 by ZF_LANG1:76;

A54: 3 <> k by A22, A42;

then A55: x. 3 <> x. k by ZF_LANG1:76;

then not x. k in {(x. 3)} by TARSKI:def 1;

then A56: not x. k in variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) by A52, A48, XBOOLE_0:def 3;

then M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) by A20, Th5;

hence A57: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) by A38, A56, A34, A39, A26, Th12; :: thesis: def_func' (H,v1) = def_func' (H2,v2)

now :: thesis: for e being Element of M holds (def_func' (H2,v2)) . e = (def_func' (H1,v9)) . e

hence
def_func' (H2,v2) = def_func' (H,v1)
by A21; :: thesis: verumlet e be Element of M; :: thesis: (def_func' (H2,v2)) . e = (def_func' (H1,v9)) . e

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: verum

end;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: verum

now :: thesis: ( ( i = 3 or i = 4 ) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )

hence
ex H2 being ZF-formula ex v2 being Function of VAR,M st ( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )

assume A73:
( i = 3 or i = 4 )
; :: thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

thus ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) :: thesis: verum

end;( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

thus ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) :: thesis: verum

proof

consider H2 being ZF-formula, v2 being Function of VAR,M such that

A74: for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds

j = 4 and

A75: not x. 0 in Free H2 and

A76: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and

A77: def_func' (H,v1) = def_func' (H2,v2) by A2, A3, A4;

take H2 ; :: thesis: ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

take v2 ; :: thesis: ( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds

j = 4 :: thesis: ( 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) )

end;A74: for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds

j = 4 and

A75: not x. 0 in Free H2 and

A76: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and

A77: def_func' (H,v1) = def_func' (H2,v2) by A2, A3, A4;

take H2 ; :: thesis: ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

take v2 ; :: thesis: ( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )

thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds

j = 4 :: thesis: ( 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) )

proof

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: verum
let j be Element of NAT ; :: thesis: ( j < i + 1 & x. j in variables_in H2 & not j = 3 implies j = 4 )

assume that

A78: j < i + 1 and

A79: x. j in variables_in H2 ; :: thesis: ( j = 3 or j = 4 )

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: verum

end;assume that

A78: j < i + 1 and

A79: x. j in variables_in H2 ; :: thesis: ( j = 3 or j = 4 )

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: verum

( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) by A12, A5; :: thesis: verum

proof

for i being Nat holds S
let H be ZF-formula; :: thesis: S_{1}[H, 0 ]

let v1 be Function of VAR,M; :: thesis: ( not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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 < 0 & 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' (H,v1) = def_func' (H2,v2) ) )

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: ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < 0 & 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' (H,v1) = def_func' (H2,v2) )

take H ; :: thesis: ex v2 being Function of VAR,M st

( ( 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,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H,v2) )

take v1 ; :: thesis: ( ( 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) )

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: verum

end;let v1 be Function of VAR,M; :: thesis: ( not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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 < 0 & 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' (H,v1) = def_func' (H2,v2) ) )

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: ex H2 being ZF-formula ex v2 being Function of VAR,M st

( ( for j being Element of NAT st j < 0 & 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' (H,v1) = def_func' (H2,v2) )

take H ; :: thesis: ex v2 being Function of VAR,M st

( ( 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,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H,v2) )

take v1 ; :: thesis: ( ( 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) )

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: verum

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 < 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) ) ) ; :: thesis: verum