zfmodel2.miz



    begin

    reserve x,y,z,x1,x2,x3,x4,y1,y2,s for Variable,

M for non empty set,

a,b for set,

i,j,k for Element of NAT ,

m,m1,m2,m3,m4 for Element of M,

H,H1,H2 for ZF-formula,

v,v9,v1,v2 for Function of VAR , M;

    theorem :: ZFMODEL2:1

    

     Th1: ( Free (H / (x,y))) c= ((( Free H) \ {x}) \/ {y})

    proof

      defpred P[ ZF-formula] means ( Free ($1 / (x,y))) c= ((( Free $1) \ {x}) \/ {y});

      

       A1: for x1, x2 holds P[(x1 '=' x2)] & P[(x1 'in' x2)]

      proof

        let x1, x2;

        

         A2: x2 = x or x2 <> x;

        x1 = x or x1 <> x;

        then

        consider y1, y2 such that

         A3: x1 <> x & x2 <> x & y1 = x1 & y2 = x2 or x1 = x & x2 <> x & y1 = y & y2 = x2 or x1 <> x & x2 = x & y1 = x1 & y2 = y or x1 = x & x2 = x & y1 = y & y2 = y by A2;

        

         A4: {y1, y2} c= (( {x1, x2} \ {x}) \/ {y})

        proof

          let a be object;

          assume a in {y1, y2};

          then (a = x1 or a = x2) & a <> x or a = y by A3, TARSKI:def 2;

          then a in {x1, x2} & not a in {x} or a in {y} by TARSKI:def 1, TARSKI:def 2;

          then a in ( {x1, x2} \ {x}) or a in {y} by XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

        ((x1 'in' x2) / (x,y)) = (y1 'in' y2) by A3, ZF_LANG1: 154;

        then

         A5: ( Free ((x1 'in' x2) / (x,y))) = {y1, y2} by ZF_LANG1: 59;

        ((x1 '=' x2) / (x,y)) = (y1 '=' y2) by A3, ZF_LANG1: 152;

        then ( Free ((x1 '=' x2) / (x,y))) = {y1, y2} by ZF_LANG1: 58;

        hence thesis by A5, A4, ZF_LANG1: 58, ZF_LANG1: 59;

      end;

      

       A6: for H1, H2 st P[H1] & P[H2] holds P[(H1 '&' H2)]

      proof

        let H1, H2;

        assume that

         A7: P[H1] and

         A8: P[H2];

        

         A9: ( Free ((H1 / (x,y)) '&' (H2 / (x,y)))) = (( Free (H1 / (x,y))) \/ ( Free (H2 / (x,y)))) by ZF_LANG1: 61;

        

         A10: (((( Free H1) \ {x}) \/ {y}) \/ ((( Free H2) \ {x}) \/ {y})) c= (((( Free H1) \/ ( Free H2)) \ {x}) \/ {y})

        proof

          let a be object;

          assume a in (((( Free H1) \ {x}) \/ {y}) \/ ((( Free H2) \ {x}) \/ {y}));

          then a in ((( Free H1) \ {x}) \/ {y}) or a in ((( Free H2) \ {x}) \/ {y}) by XBOOLE_0:def 3;

          then a in (( Free H1) \ {x}) or a in (( Free H2) \ {x}) or a in {y} by XBOOLE_0:def 3;

          then (a in ( Free H1) or a in ( Free H2)) & not a in {x} or a in {y} by XBOOLE_0:def 5;

          then a in (( Free H1) \/ ( Free H2)) & not a in {x} or a in {y} by XBOOLE_0:def 3;

          then a in ((( Free H1) \/ ( Free H2)) \ {x}) or a in {y} by XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

        

         A11: ((H1 '&' H2) / (x,y)) = ((H1 / (x,y)) '&' (H2 / (x,y))) by ZF_LANG1: 158;

        

         A12: ( Free (H1 '&' H2)) = (( Free H1) \/ ( Free H2)) by ZF_LANG1: 61;

        (( Free (H1 / (x,y))) \/ ( Free (H2 / (x,y)))) c= (((( Free H1) \ {x}) \/ {y}) \/ ((( Free H2) \ {x}) \/ {y})) by A7, A8, XBOOLE_1: 13;

        hence thesis by A9, A12, A11, A10, XBOOLE_1: 1;

      end;

      

       A13: for H, z st P[H] holds P[( All (z,H))]

      proof

        let H, z;

        

         A14: ( Free ( All (z,H))) = (( Free H) \ {z}) by ZF_LANG1: 62;

        z = x or z <> x;

        then

        consider s such that

         A15: z = x & s = y or z <> x & s = z;

        

         A16: (((( Free H) \ {x}) \/ {y}) \ {s}) c= (((( Free H) \ {z}) \ {x}) \/ {y})

        proof

          let a be object;

          assume

           A17: a in (((( Free H) \ {x}) \/ {y}) \ {s});

          then a in (( Free H) \ {x}) or a in {y} by XBOOLE_0:def 3;

          then a in ( Free H) & not a in {z} & not a in {x} or a in {y} by A15, A17, XBOOLE_0:def 5;

          then a in (( Free H) \ {z}) & not a in {x} or a in {y} by XBOOLE_0:def 5;

          then a in ((( Free H) \ {z}) \ {x}) or a in {y} by XBOOLE_0:def 5;

          hence thesis by XBOOLE_0:def 3;

        end;

        assume P[H];

        then

         A18: (( Free (H / (x,y))) \ {s}) c= (((( Free H) \ {x}) \/ {y}) \ {s}) by XBOOLE_1: 33;

        

         A19: ( Free ( All (s,(H / (x,y))))) = (( Free (H / (x,y))) \ {s}) by ZF_LANG1: 62;

        (( All (z,H)) / (x,y)) = ( All (s,(H / (x,y)))) by A15, ZF_LANG1: 159, ZF_LANG1: 160;

        hence thesis by A19, A14, A18, A16, XBOOLE_1: 1;

      end;

      

       A20: for H st P[H] holds P[( 'not' H)]

      proof

        let H;

        

         A21: ( Free ( 'not' H)) = ( Free H) by ZF_LANG1: 60;

        ( Free ( 'not' (H / (x,y)))) = ( Free (H / (x,y))) by ZF_LANG1: 60;

        hence thesis by A21, ZF_LANG1: 156;

      end;

      for H holds P[H] from ZF_LANG1:sch 1( A1, A20, A6, A13);

      hence thesis;

    end;

    theorem :: ZFMODEL2:2

    

     Th2: not y in ( variables_in H) implies (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))

    proof

      defpred P[ ZF-formula] means not y in ( variables_in $1) implies (x in ( Free $1) implies ( Free ($1 / (x,y))) = ((( Free $1) \ {x}) \/ {y})) & ( not x in ( Free $1) implies ( Free ($1 / (x,y))) = ( Free $1));

      

       A1: for H1, H2 st P[H1] & P[H2] holds P[(H1 '&' H2)]

      proof

        let H1, H2;

        assume that

         A2: P[H1] and

         A3: P[H2] and

         A4: not y in ( variables_in (H1 '&' H2));

        

         A5: ( Free ((H1 / (x,y)) '&' (H2 / (x,y)))) = (( Free (H1 / (x,y))) \/ ( Free (H2 / (x,y)))) by ZF_LANG1: 61;

        set H = (H1 '&' H2);

        

         A6: ( Free (H1 '&' H2)) = (( Free H1) \/ ( Free H2)) by ZF_LANG1: 61;

        

         A7: ( variables_in (H1 '&' H2)) = (( variables_in H1) \/ ( variables_in H2)) by ZF_LANG1: 141;

        

         A8: (H / (x,y)) = ((H1 / (x,y)) '&' (H2 / (x,y))) by ZF_LANG1: 158;

        thus x in ( Free H) implies ( Free (H / (x,y))) = ((( Free H) \ {x}) \/ {y})

        proof

          assume

           A9: x in ( Free H);

           A10:

          now

            assume

             A11: not x in ( Free H1);

            then ( Free H1) = (( Free H1) \ {x}) by ZFMISC_1: 57;

            

            hence ( Free (H / (x,y))) = (((( Free H1) \ {x}) \/ (( Free H2) \ {x})) \/ {y}) by A2, A3, A4, A6, A5, A7, A8, A9, A11, XBOOLE_0:def 3, XBOOLE_1: 4

            .= ((( Free H) \ {x}) \/ {y}) by A6, XBOOLE_1: 42;

          end;

           A12:

          now

            assume

             A13: not x in ( Free H2);

            then ( Free H2) = (( Free H2) \ {x}) by ZFMISC_1: 57;

            

            hence ( Free (H / (x,y))) = (((( Free H1) \ {x}) \/ (( Free H2) \ {x})) \/ {y}) by A2, A3, A4, A6, A5, A7, A8, A9, A13, XBOOLE_0:def 3, XBOOLE_1: 4

            .= ((( Free H) \ {x}) \/ {y}) by A6, XBOOLE_1: 42;

          end;

          now

            assume that

             A14: x in ( Free H1) and

             A15: x in ( Free H2);

            

            thus ( Free (H / (x,y))) = ((( {y} \/ (( Free H1) \ {x})) \/ (( Free H2) \ {x})) \/ {y}) by A2, A3, A4, A5, A7, A8, A14, A15, XBOOLE_0:def 3, XBOOLE_1: 4

            .= (( {y} \/ ((( Free H1) \ {x}) \/ (( Free H2) \ {x}))) \/ {y}) by XBOOLE_1: 4

            .= (((( Free H) \ {x}) \/ {y}) \/ {y}) by A6, XBOOLE_1: 42

            .= ((( Free H) \ {x}) \/ ( {y} \/ {y})) by XBOOLE_1: 4

            .= ((( Free H) \ {x}) \/ {y});

          end;

          hence thesis by A10, A12;

        end;

        assume not x in ( Free (H1 '&' H2));

        hence thesis by A2, A3, A4, A6, A5, A7, XBOOLE_0:def 3, ZF_LANG1: 158;

      end;

      

       A16: for H, z st P[H] holds P[( All (z,H))]

      proof

        let H, z;

        assume that

         A17: P[H] and

         A18: not y in ( variables_in ( All (z,H)));

        set G = (( All (z,H)) / (x,y));

        

         A19: ( Free ( All (z,H))) = (( Free H) \ {z}) by ZF_LANG1: 62;

        z = x or z <> x;

        then

        consider s such that

         A20: z = x & s = y or z <> x & s = z;

        

         A21: G = ( All (s,(H / (x,y)))) by A20, ZF_LANG1: 159, ZF_LANG1: 160;

        

         A22: ( Free ( All (s,(H / (x,y))))) = (( Free (H / (x,y))) \ {s}) by ZF_LANG1: 62;

        

         A23: ( variables_in ( All (z,H))) = (( variables_in H) \/ {z}) by ZF_LANG1: 142;

        thus x in ( Free ( All (z,H))) implies ( Free G) = ((( Free ( All (z,H))) \ {x}) \/ {y})

        proof

          assume

           A24: x in ( Free ( All (z,H)));

          then

           A25: not x in {z} by A19, XBOOLE_0:def 5;

          thus ( Free G) c= ((( Free ( All (z,H))) \ {x}) \/ {y})

          proof

            let a be object;

            assume

             A26: a in ( Free G);

            then a in ((( Free H) \ {x}) \/ {y}) by A17, A18, A19, A22, A23, A21, A24, XBOOLE_0:def 3, XBOOLE_0:def 5;

            then a in (( Free H) \ {x}) or a in {y} by XBOOLE_0:def 3;

            then

             A27: a in ( Free H) & not a in {x} or a in {y} by XBOOLE_0:def 5;

             not a in {z} by A20, A22, A21, A25, A26, TARSKI:def 1, XBOOLE_0:def 5;

            then a in ( Free ( All (z,H))) & not a in {x} or a in {y} by A19, A27, XBOOLE_0:def 5;

            then a in (( Free ( All (z,H))) \ {x}) or a in {y} by XBOOLE_0:def 5;

            hence thesis by XBOOLE_0:def 3;

          end;

          let a be object;

          assume a in ((( Free ( All (z,H))) \ {x}) \/ {y});

          then a in (( Free ( All (z,H))) \ {x}) or a in {y} by XBOOLE_0:def 3;

          then

           A28: a in ( Free ( All (z,H))) & not a in {x} or a in {y} & a = y by TARSKI:def 1, XBOOLE_0:def 5;

          then a in ( Free H) & not a in {x} or a in {y} by A19, XBOOLE_0:def 5;

          then a in (( Free H) \ {x}) or a in {y} by XBOOLE_0:def 5;

          then

           A29: a in ((( Free H) \ {x}) \/ {y}) by XBOOLE_0:def 3;

           not a in {z} by A18, A19, A23, A28, XBOOLE_0:def 3, XBOOLE_0:def 5;

          hence thesis by A20, A17, A18, A19, A22, A23, A21, A24, A25, A29, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5;

        end;

        assume not x in ( Free ( All (z,H)));

        then

         A30: not x in ( Free H) or x in {z} by A19, XBOOLE_0:def 5;

        

         A31: ( Free ( All (z,H))) c= ( variables_in ( All (z,H))) by ZF_LANG1: 151;

         A32:

        now

          assume

           A33: x in ( Free H);

          thus ( Free G) = ( Free ( All (z,H)))

          proof

            thus ( Free G) c= ( Free ( All (z,H)))

            proof

              let a be object;

              assume

               A34: a in ( Free G);

              then

               A35: not a in {y} by A20, A22, A21, A30, A33, TARSKI:def 1, XBOOLE_0:def 5;

              a in ((( Free H) \ {z}) \/ {y}) by A20, A17, A18, A22, A23, A21, A30, A33, A34, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5;

              hence thesis by A19, A35, XBOOLE_0:def 3;

            end;

            let a be object;

            assume

             A36: a in ( Free ( All (z,H)));

            then a <> y by A18, A31;

            then

             A37: not a in {y} by TARSKI:def 1;

            a in ((( Free H) \ {x}) \/ {y}) by A20, A19, A30, A33, A36, TARSKI:def 1, XBOOLE_0:def 3;

            hence thesis by A20, A17, A18, A22, A23, A21, A30, A33, A37, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5;

          end;

        end;

        now

          assume not x in ( Free H);

          then ( Free G) = ((( Free H) \ {z}) \ {y}) & not y in ( Free ( All (z,H))) or ( Free G) = (( Free H) \ {z}) by A20, A17, A18, A22, A23, A21, A31, XBOOLE_0:def 3, ZFMISC_1: 57;

          hence thesis by A19, ZFMISC_1: 57;

        end;

        hence thesis by A32;

      end;

      

       A38: for x1, x2 holds P[(x1 '=' x2)] & P[(x1 'in' x2)]

      proof

        let x1, x2;

        

         A39: x2 = x or x2 <> x;

        x1 = x or x1 <> x;

        then

        consider y1, y2 such that

         A40: x1 <> x & x2 <> x & y1 = x1 & y2 = x2 or x1 = x & x2 <> x & y1 = y & y2 = x2 or x1 <> x & x2 = x & y1 = x1 & y2 = y or x1 = x & x2 = x & y1 = y & y2 = y by A39;

        ((x1 '=' x2) / (x,y)) = (y1 '=' y2) by A40, ZF_LANG1: 152;

        then

         A41: ( Free ((x1 '=' x2) / (x,y))) = {y1, y2} by ZF_LANG1: 58;

        

         A42: ( Free (x1 '=' x2)) = {x1, x2} by ZF_LANG1: 58;

        

         A43: ( variables_in (x1 '=' x2)) = {x1, x2} by ZF_LANG1: 138;

        thus P[(x1 '=' x2)]

        proof

          assume not y in ( variables_in (x1 '=' x2));

          thus x in ( Free (x1 '=' x2)) implies ( Free ((x1 '=' x2) / (x,y))) = ((( Free (x1 '=' x2)) \ {x}) \/ {y})

          proof

            assume

             A44: x in ( Free (x1 '=' x2));

            thus ( Free ((x1 '=' x2) / (x,y))) c= ((( Free (x1 '=' x2)) \ {x}) \/ {y}) by Th1;

            let a be object;

            assume a in ((( Free (x1 '=' x2)) \ {x}) \/ {y});

            then a in (( Free (x1 '=' x2)) \ {x}) or a in {y} by XBOOLE_0:def 3;

            then a in ( Free (x1 '=' x2)) & not a in {x} or a in {y} by XBOOLE_0:def 5;

            then (a = x1 or a = x2) & a <> x or a = y by A42, TARSKI:def 1, TARSKI:def 2;

            hence thesis by A40, A41, A42, A44, TARSKI:def 2;

          end;

          assume not x in ( Free (x1 '=' x2));

          hence thesis by A42, A43, ZF_LANG1: 182;

        end;

        

         A45: ( Free (x1 'in' x2)) = {x1, x2} by ZF_LANG1: 59;

        assume not y in ( variables_in (x1 'in' x2));

        ((x1 'in' x2) / (x,y)) = (y1 'in' y2) by A40, ZF_LANG1: 154;

        then

         A46: ( Free ((x1 'in' x2) / (x,y))) = {y1, y2} by ZF_LANG1: 59;

        thus x in ( Free (x1 'in' x2)) implies ( Free ((x1 'in' x2) / (x,y))) = ((( Free (x1 'in' x2)) \ {x}) \/ {y})

        proof

          assume

           A47: x in ( Free (x1 'in' x2));

          thus ( Free ((x1 'in' x2) / (x,y))) c= ((( Free (x1 'in' x2)) \ {x}) \/ {y}) by Th1;

          let a be object;

          assume a in ((( Free (x1 'in' x2)) \ {x}) \/ {y});

          then a in (( Free (x1 'in' x2)) \ {x}) or a in {y} by XBOOLE_0:def 3;

          then a in ( Free (x1 'in' x2)) & not a in {x} or a in {y} by XBOOLE_0:def 5;

          then (a = x1 or a = x2) & a <> x or a = y by A45, TARSKI:def 1, TARSKI:def 2;

          hence thesis by A40, A46, A45, A47, TARSKI:def 2;

        end;

        assume not x in ( Free (x1 'in' x2));

        hence thesis by A41, A42, A46, A45, A43, ZF_LANG1: 182;

      end;

      

       A48: for H st P[H] holds P[( 'not' H)]

      proof

        let H;

        

         A49: ( Free ( 'not' H)) = ( Free H) by ZF_LANG1: 60;

        ( Free ( 'not' (H / (x,y)))) = ( Free (H / (x,y))) by ZF_LANG1: 60;

        hence thesis by A49, ZF_LANG1: 140, ZF_LANG1: 156;

      end;

      for H holds P[H] from ZF_LANG1:sch 1( A38, A48, A1, A16);

      hence thesis;

    end;

    registration

      let H;

      cluster ( variables_in H) -> finite;

      coherence

      proof

        ( variables_in H) = (( rng H) \ { 0 , 1, 2, 3, 4}) by ZF_LANG1:def 2;

        hence thesis;

      end;

    end

    theorem :: ZFMODEL2:3

    

     Th3: (ex i st for j st ( x. j) in ( variables_in H) holds j < i) & ex x st not x in ( variables_in H)

    proof

      defpred P[ ZF-formula] means ex i st for j st ( x. j) in ( variables_in $1) holds j < i;

      

       A1: for x, y holds P[(x '=' y)] & P[(x 'in' y)]

      proof

        let x, y;

        consider i such that

         A2: x = ( x. i) by ZF_LANG1: 77;

        consider j such that

         A3: y = ( x. j) by ZF_LANG1: 77;

        j <= (j + i) by NAT_1: 11;

        then

         A4: j < ((i + j) + 1) by NAT_1: 13;

        i <= (i + j) by NAT_1: 11;

        then

         A5: i < ((i + j) + 1) by NAT_1: 13;

        

         A6: ( variables_in (x '=' y)) = {x, y} by ZF_LANG1: 138;

        thus P[(x '=' y)]

        proof

          take ((i + j) + 1);

          let k be Element of NAT ;

          assume ( x. k) in ( variables_in (x '=' y));

          then ( x. k) = ( x. i) or ( x. k) = ( x. j) by A2, A3, A6, TARSKI:def 2;

          hence thesis by A5, A4, ZF_LANG1: 76;

        end;

        take ((i + j) + 1);

        let k be Element of NAT ;

        

         A7: ( variables_in (x 'in' y)) = {x, y} by ZF_LANG1: 139;

        assume ( x. k) in ( variables_in (x 'in' y));

        then ( x. k) = ( x. i) or ( x. k) = ( x. j) by A2, A3, A7, TARSKI:def 2;

        hence thesis by A5, A4, ZF_LANG1: 76;

      end;

      

       A8: for H1, H2 st P[H1] & P[H2] holds P[(H1 '&' H2)]

      proof

        let H1, H2;

        given i1 be Element of NAT such that

         A9: for j st ( x. j) in ( variables_in H1) holds j < i1;

        given i2 be Element of NAT such that

         A10: for j st ( x. j) in ( variables_in H2) holds j < i2;

        i1 <= i2 or i1 > i2;

        then

        consider i such that

         A11: i1 <= i2 & i = i2 or i1 > i2 & i = i1;

        take i;

        let j;

        assume ( x. j) in ( variables_in (H1 '&' H2));

        then ( x. j) in (( variables_in H1) \/ ( variables_in H2)) by ZF_LANG1: 141;

        then ( x. j) in ( variables_in H1) or ( x. j) in ( variables_in H2) by XBOOLE_0:def 3;

        then j < i1 or j < i2 by A9, A10;

        hence thesis by A11, XXREAL_0: 2;

      end;

      

       A12: for H, x st P[H] holds P[( All (x,H))]

      proof

        let H, x;

        given i1 be Element of NAT such that

         A13: for j st ( x. j) in ( variables_in H) holds j < i1;

        consider i2 be Element of NAT such that

         A14: x = ( x. i2) by ZF_LANG1: 77;

        i1 <= (i2 + 1) or i1 > (i2 + 1);

        then

        consider i such that

         A15: i1 <= (i2 + 1) & i = (i2 + 1) or i1 > (i2 + 1) & i = i1;

        take i;

        let j;

        assume ( x. j) in ( variables_in ( All (x,H)));

        then ( x. j) in (( variables_in H) \/ {x}) by ZF_LANG1: 142;

        then ( x. j) in ( variables_in H) or ( x. j) in {x} & (i2 + 0 ) = i2 & 0 < 1 by XBOOLE_0:def 3;

        then j < i1 or ( x. j) = ( x. i2) & i2 < (i2 + 1) by A13, A14, TARSKI:def 1, XREAL_1: 6;

        then j < i1 or j < (i2 + 1) by ZF_LANG1: 76;

        hence thesis by A15, XXREAL_0: 2;

      end;

      

       A16: for H st P[H] holds P[( 'not' H)]

      proof

        let H;

        ( variables_in ( 'not' H)) = ( variables_in H) by ZF_LANG1: 140;

        hence thesis;

      end;

      for H holds P[H] from ZF_LANG1:sch 1( A1, A16, A8, A12);

      then

      consider i such that

       A17: for j st ( x. j) in ( variables_in H) holds j < i;

      thus ex i st for j st ( x. j) in ( variables_in H) holds j < i by A17;

      take ( x. i);

      thus thesis by A17;

    end;

    theorem :: ZFMODEL2:4

    

     Th4: not x in ( variables_in H) implies ((M,v) |= H iff (M,v) |= ( All (x,H)))

    proof

      ( Free H) c= ( variables_in H) by ZF_LANG1: 151;

      then

       A1: x in ( Free H) implies x in ( variables_in H);

      (v / (x,(v . x))) = v by FUNCT_7: 35;

      hence thesis by A1, ZFMODEL1: 10, ZF_LANG1: 71;

    end;

    theorem :: ZFMODEL2:5

    

     Th5: not x in ( variables_in H) implies ((M,v) |= H iff (M,(v / (x,m))) |= H)

    proof

      

       A1: (M,(v / (x,m))) |= ( All (x,H)) implies (M,((v / (x,m)) / (x,(v . x)))) |= H by ZF_LANG1: 71;

      

       A2: ((v / (x,m)) / (x,(v . x))) = (v / (x,(v . x))) by FUNCT_7: 34;

      (M,v) |= ( All (x,H)) implies (M,(v / (x,m))) |= H by ZF_LANG1: 71;

      hence thesis by A1, A2, Th4, FUNCT_7: 35;

    end;

    theorem :: ZFMODEL2:6

    

     Th6: x <> y & y <> z & z <> x implies (((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))

    proof

      assume that

       A1: x <> y and

       A2: y <> z and

       A3: z <> x;

      

       A4: ((v / (z,m3)) / (y,m2)) = ((v / (y,m2)) / (z,m3)) by A2, FUNCT_7: 33;

      ((v / (x,m1)) / (y,m2)) = ((v / (y,m2)) / (x,m1)) by A1, FUNCT_7: 33;

      hence thesis by A3, A4, FUNCT_7: 33;

    end;

    theorem :: ZFMODEL2:7

    

     Th7: x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies ((((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))

    proof

      assume that

       A1: x1 <> x2 and

       A2: x1 <> x3 and

       A3: x1 <> x4 and

       A4: x2 <> x3 and

       A5: x2 <> x4 and

       A6: x3 <> x4;

      

       A7: ((((v / (x1,m1)) / (x3,m3)) / (x4,m4)) / (x2,m2)) = ((((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2)) by A2, A3, A6, Th6;

      

       A8: ((((v / (x2,m2)) / (x3,m3)) / (x1,m1)) / (x4,m4)) = ((((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1)) by A3, FUNCT_7: 33;

      (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) = (((v / (x2,m2)) / (x3,m3)) / (x1,m1)) by A1, A2, A4, Th6;

      hence thesis by A4, A5, A6, A8, A7, Th6;

    end;

    theorem :: ZFMODEL2:8

    

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

    proof

      

       A1: (((v / (x1,m1)) / (x2,m2)) / (x1,m)) = (((v / (x2,m2)) / (x1,m1)) / (x1,m)) or x1 = x2 by FUNCT_7: 33;

      hence (((v / (x1,m1)) / (x2,m2)) / (x1,m)) = ((v / (x2,m2)) / (x1,m)) by FUNCT_7: 34;

      x1 = x3 or x1 <> x3;

      then

       A2: ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m)) = ((((v / (x1,m1)) / (x2,m2)) / (x1,m)) / (x3,m3)) & (((v / (x2,m2)) / (x3,m3)) / (x1,m)) = (((v / (x2,m2)) / (x1,m)) / (x3,m3)) or ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m)) = (((v / (x1,m1)) / (x2,m2)) / (x1,m)) & (((v / (x2,m2)) / (x3,m3)) / (x1,m)) = ((v / (x2,m2)) / (x1,m)) by FUNCT_7: 33, FUNCT_7: 34;

      hence ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m)) = (((v / (x2,m2)) / (x3,m3)) / (x1,m)) by A1, FUNCT_7: 34;

      x1 = x4 or x1 <> x4;

      then (((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m)) = (((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m)) / (x4,m4)) & ((((v / (x2,m2)) / (x3,m3)) / (x1,m)) / (x4,m4)) = ((((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m)) or (((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m)) = ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m)) & ((((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m)) = (((v / (x2,m2)) / (x3,m3)) / (x1,m)) by FUNCT_7: 33, FUNCT_7: 34;

      hence thesis by A1, A2, FUNCT_7: 34;

    end;

    theorem :: ZFMODEL2:9

    

     Th9: not x in ( Free H) implies ((M,v) |= H iff (M,(v / (x,m))) |= H)

    proof

      

       A1: (v / (x,(v . x))) = v by FUNCT_7: 35;

      assume

       A2: not x in ( Free H);

      then (M,v) |= H implies (M,v) |= ( All (x,H)) by ZFMODEL1: 10;

      hence (M,v) |= H implies (M,(v / (x,m))) |= H by ZF_LANG1: 71;

      assume (M,(v / (x,m))) |= H;

      then

       A3: (M,(v / (x,m))) |= ( All (x,H)) by A2, ZFMODEL1: 10;

      ((v / (x,m)) / (x,(v . x))) = (v / (x,(v . x))) by FUNCT_7: 34;

      hence thesis by A3, A1, ZF_LANG1: 71;

    end;

    theorem :: ZFMODEL2:10

    

     Th10: not ( x. 0 ) in ( Free H) & (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) implies for m1, m2 holds (( def_func' (H,v)) . m1) = m2 iff (M,((v / (( x. 3),m1)) / (( x. 4),m2))) |= H

    proof

      assume that

       A1: not ( x. 0 ) in ( Free H) and

       A2: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

      let m1, m2;

      

       A3: ((v / (( x. 3),m1)) . ( x. 3)) = m1 by FUNCT_7: 128;

       A4:

      now

        let y;

        assume

         A5: (((v / (( x. 3),m1)) / (( x. 4),m2)) . y) <> (v . y);

        assume that ( x. 0 ) <> y and

         A6: ( x. 3) <> y and

         A7: ( x. 4) <> y;

        (((v / (( x. 3),m1)) / (( x. 4),m2)) . y) = ((v / (( x. 3),m1)) . y) by A7, FUNCT_7: 32;

        hence contradiction by A5, A6, FUNCT_7: 32;

      end;

      

       A8: (((v / (( x. 3),m1)) / (( x. 4),m2)) . ( x. 3)) = ((v / (( x. 3),m1)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

      (((v / (( x. 3),m1)) / (( x. 4),m2)) . ( x. 4)) = m2 by FUNCT_7: 128;

      hence thesis by A1, A2, A3, A8, A4, ZFMODEL1:def 1;

    end;

    

     Lm1: ( x. 0 ) <> ( x. 3) by ZF_LANG1: 76;

    

     Lm2: ( x. 0 ) <> ( x. 4) by ZF_LANG1: 76;

    

     Lm3: ( x. 3) <> ( x. 4) by ZF_LANG1: 76;

    theorem :: ZFMODEL2:11

    

     Th11: ( Free H) c= {( x. 3), ( x. 4)} & M |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) implies ( def_func' (H,v)) = ( def_func (H,M))

    proof

      assume that

       A1: ( Free H) c= {( x. 3), ( x. 4)} and

       A2: M |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

      

       A3: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) by A2;

      let a be Element of M;

      set r = (( def_func' (H,v)) . a);

      

       A4: (((v / (( x. 3),a)) / (( x. 4),r)) . ( x. 3)) = ((v / (( x. 3),a)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

       not ( x. 0 ) in ( Free H) by A1, Lm1, Lm2, TARSKI:def 2;

      then

       A5: (M,((v / (( x. 3),a)) / (( x. 4),r))) |= H by A3, Th10;

      

       A6: ((v / (( x. 3),a)) . ( x. 3)) = a by FUNCT_7: 128;

      (((v / (( x. 3),a)) / (( x. 4),r)) . ( x. 4)) = r by FUNCT_7: 128;

      hence (( def_func' (H,v)) . a) = (( def_func (H,M)) . a) by A1, A2, A5, A4, A6, ZFMODEL1:def 2;

    end;

    theorem :: ZFMODEL2:12

    

     Th12: not x in ( variables_in H) implies ((M,v) |= (H / (y,x)) iff (M,(v / (y,(v . x)))) |= H)

    proof

      defpred V[ ZF-formula] means not x in ( variables_in $1) implies for v holds (M,v) |= ($1 / (y,x)) iff (M,(v / (y,(v . x)))) |= $1;

      

       A1: for x1, x2 holds V[(x1 '=' x2)] & V[(x1 'in' x2)]

      proof

        let x1, x2;

        

         A2: x2 = y or x2 <> y;

        

         A3: x1 = y or x1 <> y;

        thus V[(x1 '=' x2)]

        proof

          assume not x in ( variables_in (x1 '=' x2));

          let v;

          consider y1, y2 such that

           A4: x1 <> y & x2 <> y & y1 = x1 & y2 = x2 or x1 = y & x2 <> y & y1 = x & y2 = x2 or x1 <> y & x2 = y & y1 = x1 & y2 = x or x1 = y & x2 = y & y1 = x & y2 = x by A3, A2;

          

           A5: ((v / (y,(v . x))) . x2) = (v . y2) by A4, FUNCT_7: 32, FUNCT_7: 128;

          

           A6: ((v / (y,(v . x))) . x1) = (v . y1) by A4, FUNCT_7: 32, FUNCT_7: 128;

          

           A7: ((x1 '=' x2) / (y,x)) = (y1 '=' y2) by A4, ZF_LANG1: 152;

          thus (M,v) |= ((x1 '=' x2) / (y,x)) implies (M,(v / (y,(v . x)))) |= (x1 '=' x2)

          proof

            assume (M,v) |= ((x1 '=' x2) / (y,x));

            then (v . y1) = (v . y2) by A7, ZF_MODEL: 12;

            hence thesis by A6, A5, ZF_MODEL: 12;

          end;

          assume (M,(v / (y,(v . x)))) |= (x1 '=' x2);

          then ((v / (y,(v . x))) . x1) = ((v / (y,(v . x))) . x2) by ZF_MODEL: 12;

          hence thesis by A7, A6, A5, ZF_MODEL: 12;

        end;

        consider y1, y2 such that

         A8: x1 <> y & x2 <> y & y1 = x1 & y2 = x2 or x1 = y & x2 <> y & y1 = x & y2 = x2 or x1 <> y & x2 = y & y1 = x1 & y2 = x or x1 = y & x2 = y & y1 = x & y2 = x by A3, A2;

        assume not x in ( variables_in (x1 'in' x2));

        let v;

        

         A9: ((v / (y,(v . x))) . x1) = (v . y1) by A8, FUNCT_7: 32, FUNCT_7: 128;

        

         A10: ((v / (y,(v . x))) . x2) = (v . y2) by A8, FUNCT_7: 32, FUNCT_7: 128;

        

         A11: ((x1 'in' x2) / (y,x)) = (y1 'in' y2) by A8, ZF_LANG1: 154;

        thus (M,v) |= ((x1 'in' x2) / (y,x)) implies (M,(v / (y,(v . x)))) |= (x1 'in' x2)

        proof

          assume (M,v) |= ((x1 'in' x2) / (y,x));

          then (v . y1) in (v . y2) by A11, ZF_MODEL: 13;

          hence thesis by A9, A10, ZF_MODEL: 13;

        end;

        assume (M,(v / (y,(v . x)))) |= (x1 'in' x2);

        then ((v / (y,(v . x))) . x1) in ((v / (y,(v . x))) . x2) by ZF_MODEL: 13;

        hence thesis by A11, A9, A10, ZF_MODEL: 13;

      end;

      

       A12: for H1, H2 st V[H1] & V[H2] holds V[(H1 '&' H2)]

      proof

        let H1, H2 such that

         A13: not x in ( variables_in H1) implies for v holds (M,v) |= (H1 / (y,x)) iff (M,(v / (y,(v . x)))) |= H1 and

         A14: not x in ( variables_in H2) implies for v holds (M,v) |= (H2 / (y,x)) iff (M,(v / (y,(v . x)))) |= H2;

        assume not x in ( variables_in (H1 '&' H2));

        then

         A15: not x in (( variables_in H1) \/ ( variables_in H2)) by ZF_LANG1: 141;

        let v;

        thus (M,v) |= ((H1 '&' H2) / (y,x)) implies (M,(v / (y,(v . x)))) |= (H1 '&' H2)

        proof

          assume (M,v) |= ((H1 '&' H2) / (y,x));

          then

           A16: (M,v) |= ((H1 / (y,x)) '&' (H2 / (y,x))) by ZF_LANG1: 158;

          then (M,v) |= (H2 / (y,x)) by ZF_MODEL: 15;

          then

           A17: (M,(v / (y,(v . x)))) |= H2 by A14, A15, XBOOLE_0:def 3;

          (M,v) |= (H1 / (y,x)) by A16, ZF_MODEL: 15;

          then (M,(v / (y,(v . x)))) |= H1 by A13, A15, XBOOLE_0:def 3;

          hence thesis by A17, ZF_MODEL: 15;

        end;

        assume

         A18: (M,(v / (y,(v . x)))) |= (H1 '&' H2);

        then (M,(v / (y,(v . x)))) |= H2 by ZF_MODEL: 15;

        then

         A19: (M,v) |= (H2 / (y,x)) by A14, A15, XBOOLE_0:def 3;

        (M,(v / (y,(v . x)))) |= H1 by A18, ZF_MODEL: 15;

        then (M,v) |= (H1 / (y,x)) by A13, A15, XBOOLE_0:def 3;

        then (M,v) |= ((H1 / (y,x)) '&' (H2 / (y,x))) by A19, ZF_MODEL: 15;

        hence thesis by ZF_LANG1: 158;

      end;

      

       A20: for H, z st V[H] holds V[( All (z,H))]

      proof

        let H, z such that

         A21: not x in ( variables_in H) implies for v holds (M,v) |= (H / (y,x)) iff (M,(v / (y,(v . x)))) |= H;

        z = y or z <> y;

        then

        consider s be Variable such that

         A22: z = y & s = x or z <> y & s = z;

        assume

         A23: not x in ( variables_in ( All (z,H)));

        then

         A24: not x in (( variables_in H) \/ {z}) by ZF_LANG1: 142;

        then not x in {z} by XBOOLE_0:def 3;

        then

         A25: x <> z by TARSKI:def 1;

        let v;

        ( Free H) c= ( variables_in H) by ZF_LANG1: 151;

        then

         A26: not x in ( Free H) by A24, XBOOLE_0:def 3;

        thus (M,v) |= (( All (z,H)) / (y,x)) implies (M,(v / (y,(v . x)))) |= ( All (z,H))

        proof

          assume (M,v) |= (( All (z,H)) / (y,x));

          then

           A27: (M,v) |= ( All (s,(H / (y,x)))) by A22, ZF_LANG1: 159, ZF_LANG1: 160;

           A28:

          now

            assume that

             A29: z = y and

             A30: s = x;

            now

              let m;

              

               A31: ((v / (x,m)) . x) = m by FUNCT_7: 128;

              (M,(v / (x,m))) |= (H / (y,x)) by A27, A30, ZF_LANG1: 71;

              then

               A32: (M,((v / (x,m)) / (y,((v / (x,m)) . x)))) |= H by A21, A24, XBOOLE_0:def 3;

              ((v / (x,m)) / (y,m)) = ((v / (y,m)) / (x,m)) by A25, A29, FUNCT_7: 33;

              then (M,((v / (y,m)) / (x,m))) |= ( All (x,H)) by A26, A32, A31, ZFMODEL1: 10;

              then

               A33: (M,(((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)))) |= H by ZF_LANG1: 71;

              (((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x))) = ((v / (y,m)) / (x,((v / (y,m)) . x))) by FUNCT_7: 34;

              hence (M,(v / (y,m))) |= H by A33, FUNCT_7: 35;

            end;

            then (M,v) |= ( All (y,H)) by ZF_LANG1: 71;

            hence thesis by A29, ZF_LANG1: 72;

          end;

          now

            assume that

             A34: z <> y and

             A35: s = z;

            now

              let m;

              (M,(v / (z,m))) |= (H / (y,x)) by A27, A35, ZF_LANG1: 71;

              then

               A36: (M,((v / (z,m)) / (y,((v / (z,m)) . x)))) |= H by A21, A24, XBOOLE_0:def 3;

              ((v / (z,m)) . x) = (v . x) by A25, FUNCT_7: 32;

              hence (M,((v / (y,(v . x))) / (z,m))) |= H by A34, A36, FUNCT_7: 33;

            end;

            hence thesis by ZF_LANG1: 71;

          end;

          hence thesis by A22, A28;

        end;

        assume

         A37: (M,(v / (y,(v . x)))) |= ( All (z,H));

        ( Free ( All (z,H))) c= ( variables_in ( All (z,H))) by ZF_LANG1: 151;

        then

         A38: not x in ( Free ( All (z,H))) by A23;

         A39:

        now

          assume that

           A40: z = y and s = x;

          (M,v) |= ( All (y,H)) by A37, A40, ZF_LANG1: 72;

          then

           A41: (M,v) |= ( All (x,( All (y,H)))) by A38, A40, ZFMODEL1: 10;

          now

            let m;

            (M,(v / (x,m))) |= ( All (y,H)) by A41, ZF_LANG1: 71;

            then

             A42: (M,((v / (x,m)) / (y,m))) |= H by ZF_LANG1: 71;

            ((v / (x,m)) . x) = m by FUNCT_7: 128;

            hence (M,(v / (x,m))) |= (H / (y,x)) by A21, A24, A42, XBOOLE_0:def 3;

          end;

          then (M,v) |= ( All (x,(H / (y,x)))) by ZF_LANG1: 71;

          hence thesis by A40, ZF_LANG1: 160;

        end;

        now

          assume that

           A43: z <> y and s = z;

          now

            let m;

            (M,((v / (y,(v . x))) / (z,m))) |= H by A37, ZF_LANG1: 71;

            then (M,((v / (z,m)) / (y,(v . x)))) |= H by A43, FUNCT_7: 33;

            then (M,((v / (z,m)) / (y,((v / (z,m)) . x)))) |= H by A25, FUNCT_7: 32;

            hence (M,(v / (z,m))) |= (H / (y,x)) by A21, A24, XBOOLE_0:def 3;

          end;

          then (M,v) |= ( All (z,(H / (y,x)))) by ZF_LANG1: 71;

          hence thesis by A43, ZF_LANG1: 159;

        end;

        hence thesis by A22, A39;

      end;

      

       A44: for H st V[H] holds V[( 'not' H)]

      proof

        let H such that

         A45: not x in ( variables_in H) implies for v holds (M,v) |= (H / (y,x)) iff (M,(v / (y,(v . x)))) |= H;

        assume

         A46: not x in ( variables_in ( 'not' H));

        let v;

        thus (M,v) |= (( 'not' H) / (y,x)) implies (M,(v / (y,(v . x)))) |= ( 'not' H)

        proof

          assume (M,v) |= (( 'not' H) / (y,x));

          then (M,v) |= ( 'not' (H / (y,x))) by ZF_LANG1: 156;

          then not (M,v) |= (H / (y,x)) by ZF_MODEL: 14;

          then not (M,(v / (y,(v . x)))) |= H by A45, A46, ZF_LANG1: 140;

          hence thesis by ZF_MODEL: 14;

        end;

        assume (M,(v / (y,(v . x)))) |= ( 'not' H);

        then not (M,(v / (y,(v . x)))) |= H by ZF_MODEL: 14;

        then not (M,v) |= (H / (y,x)) by A45, A46, ZF_LANG1: 140;

        then (M,v) |= ( 'not' (H / (y,x))) by ZF_MODEL: 14;

        hence thesis by ZF_LANG1: 156;

      end;

      for H holds V[H] from ZF_LANG1:sch 1( A1, A44, A12, A20);

      hence thesis;

    end;

    theorem :: ZFMODEL2:13

    

     Th13: not x in ( variables_in H) & (M,v) |= H implies (M,(v / (x,(v . y)))) |= (H / (y,x))

    proof

      assume that

       A1: not x in ( variables_in H) and

       A2: (M,v) |= H;

      

       A3: ((v / (x,(v . y))) . x) = (v . y) by FUNCT_7: 128;

      x = y or x <> y;

      then

       A4: ((v / (x,(v . y))) / (y,(v . y))) = ((v / (y,(v . y))) / (x,(v . y))) by FUNCT_7: 33;

      

       A5: (v / (y,(v . y))) = v by FUNCT_7: 35;

      (M,(v / (x,(v . y)))) |= H by A1, A2, Th5;

      hence thesis by A1, A4, A3, A5, Th12;

    end;

    theorem :: ZFMODEL2:14

    

     Th14: 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) & not y in ( Free H) & x <> ( x. 0 ) & x <> ( x. 3) & x <> ( x. 4) implies 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)))))

    proof

      

       A1: ( x. 0 ) <> ( x. 4) by ZF_LANG1: 76;

      

       A2: ( x. 3) <> ( x. 4) by ZF_LANG1: 76;

      set F = (H / (y,x)), f = (v / (x,(v . y)));

      assume that

       A3: not ( x. 0 ) in ( Free H) and

       A4: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) and

       A5: not x in ( variables_in H) and

       A6: not y in ( Free H) and

       A7: x <> ( x. 0 ) and

       A8: x <> ( x. 3) and

       A9: x <> ( x. 4);

      ( Free F) c= ( variables_in F) & not ( x. 0 ) in ( variables_in F) or not ( x. 0 ) in {x} & not ( x. 0 ) in (( Free H) \ {y}) by A3, A7, TARSKI:def 1, XBOOLE_0:def 5;

      then not ( x. 0 ) in ( Free F) or ( Free F) c= ((( Free H) \ {y}) \/ {x}) & not ( x. 0 ) in ((( Free H) \ {y}) \/ {x}) by Th1, XBOOLE_0:def 3;

      hence

       A10: not ( x. 0 ) in ( Free F);

      

       A11: ( x. 0 ) <> ( x. 3) by ZF_LANG1: 76;

      now

        let m3;

        (M,(v / (( x. 3),m3))) |= ( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))) by A4, ZF_LANG1: 71;

        then

        consider m such that

         A12: (M,((v / (( x. 3),m3)) / (( x. 0 ),m))) |= ( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))) by ZF_LANG1: 73;

        set f1 = ((f / (( x. 3),m3)) / (( x. 0 ),m));

        now

          let m4;

          

           A13: ((((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4)) . ( x. 4)) = m4 by FUNCT_7: 128;

          

           A14: ((((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4)) . ( x. 0 )) = (((v / (( x. 3),m3)) / (( x. 0 ),m)) . ( x. 0 )) by FUNCT_7: 32, ZF_LANG1: 76;

          

           A15: ((f1 / (( x. 4),m4)) . ( x. 0 )) = (f1 . ( x. 0 )) by FUNCT_7: 32, ZF_LANG1: 76;

          

           A16: ((f1 / (( x. 4),m4)) . ( x. 4)) = m4 by FUNCT_7: 128;

          

           A17: (f1 . ( x. 0 )) = m by FUNCT_7: 128;

          

           A18: (((v / (( x. 3),m3)) / (( x. 0 ),m)) . ( x. 0 )) = m by FUNCT_7: 128;

          

           A19: (M,(((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4))) |= (H <=> (( x. 4) '=' ( x. 0 ))) by A12, ZF_LANG1: 71;

           A20:

          now

            assume (M,(f1 / (( x. 4),m4))) |= (( x. 4) '=' ( x. 0 ));

            then m = m4 by A16, A15, A17, ZF_MODEL: 12;

            then (M,(((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4))) |= (( x. 4) '=' ( x. 0 )) by A13, A14, A18, ZF_MODEL: 12;

            then (M,(((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4))) |= H by A19, ZF_MODEL: 19;

            then (M,((((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4)) / (x,(v . y)))) |= H by A5, Th5;

            then (M,(f1 / (( x. 4),m4))) |= H by A7, A8, A9, A11, A1, A2, Th7;

            then (M,((f1 / (( x. 4),m4)) / (y,((f1 / (( x. 4),m4)) . x)))) |= H by A6, Th9;

            hence (M,(f1 / (( x. 4),m4))) |= F by A5, Th12;

          end;

          now

            assume (M,(f1 / (( x. 4),m4))) |= F;

            then (M,((f1 / (( x. 4),m4)) / (y,((f1 / (( x. 4),m4)) . x)))) |= H by A5, Th12;

            then (M,(f1 / (( x. 4),m4))) |= H by A6, Th9;

            then (M,((((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4)) / (x,(v . y)))) |= H by A7, A8, A9, A11, A1, A2, Th7;

            then (M,(((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4))) |= H by A5, Th5;

            then (M,(((v / (( x. 3),m3)) / (( x. 0 ),m)) / (( x. 4),m4))) |= (( x. 4) '=' ( x. 0 )) by A19, ZF_MODEL: 19;

            then m = m4 by A13, A14, A18, ZF_MODEL: 12;

            hence (M,(f1 / (( x. 4),m4))) |= (( x. 4) '=' ( x. 0 )) by A16, A15, A17, ZF_MODEL: 12;

          end;

          hence (M,(f1 / (( x. 4),m4))) |= (F <=> (( x. 4) '=' ( x. 0 ))) by A20, ZF_MODEL: 19;

        end;

        then (M,f1) |= ( All (( x. 4),(F <=> (( x. 4) '=' ( x. 0 ))))) by ZF_LANG1: 71;

        hence (M,(f / (( x. 3),m3))) |= ( Ex (( x. 0 ),( All (( x. 4),(F <=> (( x. 4) '=' ( x. 0 ))))))) by ZF_LANG1: 73;

      end;

      hence

       A21: (M,f) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(F <=> (( x. 4) '=' ( x. 0 ))))))))) by ZF_LANG1: 71;

      

       A22: ( Free H) c= ( variables_in H) by ZF_LANG1: 151;

      ( Free F) = ( Free H) by A5, A6, Th2;

      then

       A23: not x in ( Free F) by A5, A22;

      let a be Element of M;

      set a9 = (( def_func' (H,v)) . a);

      (M,((v / (( x. 3),a)) / (( x. 4),a9))) |= H by A3, A4, Th10;

      then (M,(((v / (( x. 3),a)) / (( x. 4),a9)) / (x,(v . y)))) |= H by A5, Th5;

      then (M,((f / (( x. 3),a)) / (( x. 4),a9))) |= H by A8, A9, A2, Th6;

      then (M,(((f / (( x. 3),a)) / (( x. 4),a9)) / (x,(((f / (( x. 3),a)) / (( x. 4),a9)) . y)))) |= F by A5, Th13;

      then (M,((f / (( x. 3),a)) / (( x. 4),a9))) |= F by A23, Th9;

      hence (( def_func' (H,v)) . a) = (( def_func' (F,f)) . a) by A10, A21, Th10;

    end;

    theorem :: ZFMODEL2:15

     not x in ( variables_in H) implies (M |= (H / (y,x)) iff M |= H)

    proof

      assume

       A1: not x in ( variables_in H);

      thus M |= (H / (y,x)) implies M |= H

      proof

        assume

         A2: (M,v) |= (H / (y,x));

        let v;

        

         A3: ((v / (x,(v . y))) . x) = (v . y) by FUNCT_7: 128;

        (M,(v / (x,(v . y)))) |= (H / (y,x)) by A2;

        then (M,((v / (x,(v . y))) / (y,(v . y)))) |= H by A1, A3, Th12;

        then

         A4: (M,(((v / (x,(v . y))) / (y,(v . y))) / (x,(v . x)))) |= H by A1, Th5;

        x = y or x <> y;

        then (M,((v / (x,(v . y))) / (x,(v . x)))) |= H or (M,(((v / (y,(v . y))) / (x,(v . y))) / (x,(v . x)))) |= H by A4, FUNCT_7: 33;

        then (M,(v / (x,(v . x)))) |= H or (M,((v / (y,(v . y))) / (x,(v . x)))) |= H by FUNCT_7: 34;

        then (M,(v / (x,(v . x)))) |= H by FUNCT_7: 35;

        hence thesis by FUNCT_7: 35;

      end;

      assume

       A5: (M,v) |= H;

      let v;

      (M,(v / (y,(v . x)))) |= H by A5;

      hence thesis by A1, Th12;

    end;

    theorem :: ZFMODEL2:16

    

     Th16: 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, v2 st (for j st j < i & ( x. j) in ( variables_in H2) holds j = 3 or 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))

    proof

      defpred ZF[ ZF-formula, Nat] means for v1 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, v2 st (for j st j < $2 & ( x. j) in ( variables_in H2) holds j = 3 or 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 P[ Nat] means for H holds ZF[H, $1];

      

       A1: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A2: ZF[H, i];

        let H, v1 such 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 )))))))));

        

         A5: i = 0 implies thesis

        proof

          assume

           A6: i = 0 ;

          consider k such that

           A7: for j st ( x. j) in ( variables_in H) holds j < k by Th3;

          k > 4 or not k > 4;

          then

          consider k1 be Element of NAT such that

           A8: k > 4 & k1 = k or not k > 4 & k1 = 5;

          take F = (H / (( x. 0 ),( x. k1))), (v1 / (( x. k1),(v1 . ( x. 0 ))));

          thus for j st j < (i + 1) & ( x. j) in ( variables_in F) holds j = 3 or j = 4

          proof

            let j;

            assume j < (i + 1);

            then j <= 0 by A6, NAT_1: 13;

            then j = 0 ;

            hence thesis by A8, ZF_LANG1: 76, ZF_LANG1: 184;

          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 thesis by A3, A4, A9, A10, A11, Th14;

        end;

        

         A12: i <> 0 & i <> 3 & i <> 4 implies thesis

        proof

          

           A13: ( x. 3) <> ( x. 4) by ZF_LANG1: 76;

          assume that

           A14: i <> 0 and

           A15: i <> 3 and

           A16: i <> 4;

          reconsider ii = i as Element of NAT by ORDINAL1:def 12;

          

           A17: ( x. 0 ) <> ( x. ii) by A14, ZF_LANG1: 76;

          consider H1, v9 such that

           A18: for j st j < i & ( x. j) in ( variables_in H1) holds j = 3 or 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 be Element of NAT such that

           A22: for j st ( x. j) in ( variables_in ( All (( x. 4),( x. ii),H1))) holds j < k by Th3;

          take H2 = (H1 / (( x. ii),( x. k))), v2 = (v9 / (( x. k),(v9 . ( x. ii))));

          

           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 st j < (i + 1) & ( x. j) in ( variables_in H2) holds j = 3 or j = 4

          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;

            

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

            assume j < (i + 1);

            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);

            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 thesis by A18, A27, A28, A29, A32, A33, XBOOLE_0:def 3;

          end;

          

           A34: (v2 . ( x. k)) = (v9 . ( x. ii)) by FUNCT_7: 128;

          

           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;

          

           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;

          now

            let e be Element of M;

            

             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 be 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;

          end;

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

        end;

        now

          assume

           A73: i = 3 or i = 4;

          thus thesis

          proof

            consider H2, v2 such that

             A74: for j st j < i & ( x. j) in ( variables_in H2) holds j = 3 or 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, v2;

            thus for j st j < (i + 1) & ( x. j) in ( variables_in H2) holds j = 3 or j = 4

            proof

              let j;

              assume that

               A78: j < (i + 1) and

               A79: ( x. j) in ( variables_in H2);

              j <= i by A78, NAT_1: 13;

              then j < i or j = i by XXREAL_0: 1;

              hence thesis by A73, A74, A79;

            end;

            thus thesis by A75, A76, A77;

          end;

        end;

        hence thesis by A12, A5;

      end;

      

       A80: P[ 0 ]

      proof

        let H;

        let v1 such 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 )))))))));

        take H, v1;

        thus thesis by A81, A82;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A80, A1);

      hence thesis;

    end;

    theorem :: ZFMODEL2:17

     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, v2 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))

    proof

      assume that

       A1: not ( x. 0 ) in ( Free H1) and

       A2: (M,v1) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H1 <=> (( x. 4) '=' ( x. 0 )))))))));

      consider i such that

       A3: for j st ( x. j) in ( variables_in H1) holds j < i by Th3;

      consider H2, v2 such that

       A4: for j st j < i & ( x. j) in ( variables_in H2) holds j = 3 or j = 4 and

       A5: not ( x. 0 ) in ( Free H2) and

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

       A7: ( def_func' (H1,v1)) = ( def_func' (H2,v2)) by A1, A2, Th16;

      take H2, v2;

      thus (( Free H1) /\ ( Free H2)) c= {( x. 3), ( x. 4)}

      proof

        

         A8: ( Free H2) c= ( variables_in H2) by ZF_LANG1: 151;

        let a be object;

        

         A9: ( Free H1) c= ( variables_in H1) by ZF_LANG1: 151;

        assume

         A10: a in (( Free H1) /\ ( Free H2));

        then

         A11: a in ( Free H2) by XBOOLE_0:def 4;

        reconsider x = a as Variable by A10;

        consider j such that

         A12: x = ( x. j) by ZF_LANG1: 77;

        a in ( Free H1) by A10, XBOOLE_0:def 4;

        then j = 3 or j = 4 by A3, A4, A11, A12, A9, A8;

        hence thesis by A12, TARSKI:def 2;

      end;

      thus thesis by A5, A6, A7;

    end;

    reserve F,G for Function;

    theorem :: ZFMODEL2:18

    F is_definable_in M & G is_definable_in M implies (F * G) is_definable_in M

    proof

      set x0 = ( x. 0 ), x3 = ( x. 3), x4 = ( x. 4);

      given H1 such that

       A1: ( Free H1) c= {( x. 3), ( x. 4)} and

       A2: M |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H1 <=> (( x. 4) '=' ( x. 0 ))))))))) and

       A3: F = ( def_func (H1,M));

      given H2 such that

       A4: ( Free H2) c= {( x. 3), ( x. 4)} and

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

       A6: G = ( def_func (H2,M));

      reconsider F, G as Function of M, M by A3, A6;

      consider x such that

       A7: not x in ( variables_in ( All (( x. 0 ),( x. 3),( x. 4),(H1 '&' H2)))) by Th3;

      

       A8: ( variables_in ( All (( x. 0 ),( x. 3),( x. 4),(H1 '&' H2)))) = (( variables_in (H1 '&' H2)) \/ {( x. 0 ), ( x. 3), ( x. 4)}) by ZF_LANG1: 149;

      then

       A9: not x in {( x. 0 ), ( x. 3), ( x. 4)} by A7, XBOOLE_0:def 3;

      then

       A10: x <> ( x. 3) by ENUMSET1:def 1;

      take H = ( Ex (x,((H1 / (( x. 3),x)) '&' (H2 / (( x. 4),x)))));

      thus

       A11: ( Free H) c= {( x. 3), ( x. 4)}

      proof

        let a be object;

        assume a in ( Free H);

        then

         A12: a in (( Free ((H1 / (( x. 3),x)) '&' (H2 / (( x. 4),x)))) \ {x}) by ZF_LANG1: 66;

        then a in ( Free ((H1 / (( x. 3),x)) '&' (H2 / (( x. 4),x)))) by XBOOLE_0:def 5;

        then a in (( Free (H1 / (( x. 3),x))) \/ ( Free (H2 / (( x. 4),x)))) by ZF_LANG1: 61;

        then ( Free (H1 / (( x. 3),x))) c= ((( Free H1) \ {( x. 3)}) \/ {x}) & a in ( Free (H1 / (( x. 3),x))) or ( Free (H2 / (( x. 4),x))) c= ((( Free H2) \ {( x. 4)}) \/ {x}) & a in ( Free (H2 / (( x. 4),x))) by Th1, XBOOLE_0:def 3;

        then

         A13: (( Free H1) \ {( x. 3)}) c= ( Free H1) & a in ((( Free H1) \ {( x. 3)}) \/ {x}) or (( Free H2) \ {( x. 4)}) c= ( Free H2) & a in ((( Free H2) \ {( x. 4)}) \/ {x}) by XBOOLE_1: 36;

         not a in {x} by A12, XBOOLE_0:def 5;

        then (( Free H1) \ {( x. 3)}) c= {( x. 3), ( x. 4)} & a in (( Free H1) \ {( x. 3)}) or (( Free H2) \ {( x. 4)}) c= {( x. 3), ( x. 4)} & a in (( Free H2) \ {( x. 4)}) by A1, A4, A13, XBOOLE_0:def 3;

        hence thesis;

      end;

      

       A14: x0 <> x4 by ZF_LANG1: 76;

      

       A15: x3 <> x4 by ZF_LANG1: 76;

      

       A16: x <> ( x. 4) by A9, ENUMSET1:def 1;

      ( variables_in (H1 '&' H2)) = (( variables_in H1) \/ ( variables_in H2)) by ZF_LANG1: 141;

      then

       A17: not x in (( variables_in H1) \/ ( variables_in H2)) by A7, A8, XBOOLE_0:def 3;

      then

       A18: not x in ( variables_in H1) by XBOOLE_0:def 3;

      

       A19: not x in ( variables_in H2) by A17, XBOOLE_0:def 3;

      

       A20: x0 <> x3 by ZF_LANG1: 76;

      then

       A21: not x0 in ( Free H2) by A4, A14, TARSKI:def 2;

      thus

       A22: M |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))))

      proof

        let v;

        now

          let m3 be Element of M;

          (M,v) |= ( All (x3,( Ex (x0,( All (x4,(H2 <=> (x4 '=' x0)))))))) by A5;

          then (M,(v / (x3,m3))) |= ( Ex (x0,( All (x4,(H2 <=> (x4 '=' x0)))))) by ZF_LANG1: 71;

          then

          consider m0 be Element of M such that

           A23: (M,((v / (x3,m3)) / (x0,m0))) |= ( All (x4,(H2 <=> (x4 '=' x0)))) by ZF_LANG1: 73;

          (M,v) |= ( All (x3,( Ex (x0,( All (x4,(H1 <=> (x4 '=' x0)))))))) by A2;

          then (M,(v / (x3,m0))) |= ( Ex (x0,( All (x4,(H1 <=> (x4 '=' x0)))))) by ZF_LANG1: 71;

          then

          consider m be Element of M such that

           A24: (M,((v / (x3,m0)) / (x0,m))) |= ( All (x4,(H1 <=> (x4 '=' x0)))) by ZF_LANG1: 73;

          now

            let m4 be Element of M;

             A25:

            now

              assume (M,(((v / (x3,m3)) / (x0,m)) / (x4,m4))) |= H;

              then

              consider m9 be Element of M such that

               A26: (M,((((v / (x3,m3)) / (x0,m)) / (x4,m4)) / (x,m9))) |= ((H1 / (x3,x)) '&' (H2 / (x4,x))) by ZF_LANG1: 73;

              set v9 = ((((v / (x3,m3)) / (x0,m)) / (x4,m4)) / (x,m9));

              

               A27: (v9 . x) = m9 by FUNCT_7: 128;

              

               A28: (v9 / (x4,m9)) = ((((v / (x3,m3)) / (x0,m)) / (x,m9)) / (x4,m9)) by Th8

              .= ((((v / (x3,m3)) / (x0,m)) / (x4,m9)) / (x,m9)) by A16, FUNCT_7: 33;

              (M,v9) |= (H2 / (x4,x)) by A26, ZF_MODEL: 15;

              then (M,(v9 / (x4,m9))) |= H2 by A19, A27, Th12;

              then

               A29: (M,(((v / (x3,m3)) / (x0,m)) / (x4,m9))) |= H2 by A19, A28, Th5;

              

               A30: (((v / (x3,m3)) / (x4,m9)) / (x0,m0)) = ((((v / (x3,m3)) / (x4,m9)) / (x0,m)) / (x0,m0)) by FUNCT_7: 34;

              

               A31: ((((v / (x3,m3)) / (x0,m)) / (x4,m4)) . x0) = (((v / (x3,m3)) / (x0,m)) . x0) by FUNCT_7: 32, ZF_LANG1: 76;

              

               A32: ((((v / (x3,m0)) / (x0,m)) / (x4,m4)) . x0) = (((v / (x3,m0)) / (x0,m)) . x0) by FUNCT_7: 32, ZF_LANG1: 76;

              (M,v9) |= (H1 / (x3,x)) by A26, ZF_MODEL: 15;

              then

               A33: (M,(v9 / (x3,m9))) |= H1 by A18, A27, Th12;

              

               A34: (((v / (x3,m3)) / (x0,m0)) / (x4,m9)) = (((v / (x3,m3)) / (x4,m9)) / (x0,m0)) by FUNCT_7: 33, ZF_LANG1: 76;

              

               A35: (M,(((v / (x3,m3)) / (x0,m0)) / (x4,m9))) |= (H2 <=> (x4 '=' x0)) by A23, ZF_LANG1: 71;

              

               A36: ((((v / (x3,m3)) / (x0,m0)) / (x4,m9)) . x0) = (((v / (x3,m3)) / (x0,m0)) . x0) by FUNCT_7: 32, ZF_LANG1: 76;

              (((v / (x3,m3)) / (x0,m)) / (x4,m9)) = (((v / (x3,m3)) / (x4,m9)) / (x0,m)) by FUNCT_7: 33, ZF_LANG1: 76;

              then (M,(((v / (x3,m3)) / (x0,m0)) / (x4,m9))) |= H2 by A21, A30, A34, A29, Th9;

              then (M,(((v / (x3,m3)) / (x0,m0)) / (x4,m9))) |= (x4 '=' x0) by A35, ZF_MODEL: 19;

              then

               A37: ((((v / (x3,m3)) / (x0,m0)) / (x4,m9)) . x4) = ((((v / (x3,m3)) / (x0,m0)) / (x4,m9)) . x0) by ZF_MODEL: 12;

              

               A38: (((v / (x3,m3)) / (x0,m0)) . x0) = m0 by FUNCT_7: 128;

              ((((v / (x3,m3)) / (x0,m0)) / (x4,m9)) . x4) = m9 by FUNCT_7: 128;

              

              then (v9 / (x3,m9)) = (((((v / (x3,m3)) / (x0,m)) / (x4,m4)) / (x3,m0)) / (x,m9)) by A10, A37, A38, A36, FUNCT_7: 33

              .= ((((v / (x0,m)) / (x4,m4)) / (x3,m0)) / (x,m9)) by Th8

              .= ((((v / (x3,m0)) / (x0,m)) / (x4,m4)) / (x,m9)) by A20, A14, A15, Th6;

              then

               A39: (M,(((v / (x3,m0)) / (x0,m)) / (x4,m4))) |= H1 by A18, A33, Th5;

              (M,(((v / (x3,m0)) / (x0,m)) / (x4,m4))) |= (H1 <=> (x4 '=' x0)) by A24, ZF_LANG1: 71;

              then (M,(((v / (x3,m0)) / (x0,m)) / (x4,m4))) |= (x4 '=' x0) by A39, ZF_MODEL: 19;

              then

               A40: ((((v / (x3,m0)) / (x0,m)) / (x4,m4)) . x4) = ((((v / (x3,m0)) / (x0,m)) / (x4,m4)) . x0) by ZF_MODEL: 12;

              

               A41: (((v / (x3,m0)) / (x0,m)) . x0) = m by FUNCT_7: 128;

              

               A42: (((v / (x3,m3)) / (x0,m)) . x0) = m by FUNCT_7: 128;

              

               A43: ((((v / (x3,m3)) / (x0,m)) / (x4,m4)) . x4) = m4 by FUNCT_7: 128;

              ((((v / (x3,m0)) / (x0,m)) / (x4,m4)) . x4) = m4 by FUNCT_7: 128;

              hence (M,(((v / (x3,m3)) / (x0,m)) / (x4,m4))) |= (x4 '=' x0) by A40, A41, A43, A42, A32, A31, ZF_MODEL: 12;

            end;

            now

              set v9 = ((((v / (x3,m3)) / (x0,m)) / (x4,m4)) / (x,m0));

              

               A44: (((v / (x3,m0)) / (x0,m)) . x0) = m by FUNCT_7: 128;

              

               A45: ((((v / (x3,m3)) / (x0,m)) / (x4,m4)) . x4) = m4 by FUNCT_7: 128;

              

               A46: (M,(((v / (x3,m3)) / (x0,m0)) / (x4,m0))) |= (H2 <=> (x4 '=' x0)) by A23, ZF_LANG1: 71;

              

               A47: ((((v / (x3,m3)) / (x0,m)) / (x4,m4)) . x0) = (((v / (x3,m3)) / (x0,m)) . x0) by FUNCT_7: 32, ZF_LANG1: 76;

              assume (M,(((v / (x3,m3)) / (x0,m)) / (x4,m4))) |= (x4 '=' x0);

              then

               A48: ((((v / (x3,m3)) / (x0,m)) / (x4,m4)) . x4) = ((((v / (x3,m3)) / (x0,m)) / (x4,m4)) . x0) by ZF_MODEL: 12;

              

               A49: (((v / (x3,m3)) / (x0,m)) . x0) = m by FUNCT_7: 128;

              

               A50: ((((v / (x3,m3)) / (x0,m0)) / (x4,m0)) . x0) = (((v / (x3,m3)) / (x0,m0)) . x0) by FUNCT_7: 32, ZF_LANG1: 76;

              

               A51: (M,(((v / (x3,m0)) / (x0,m)) / (x4,m4))) |= (H1 <=> (x4 '=' x0)) by A24, ZF_LANG1: 71;

              

               A52: ((((v / (x3,m0)) / (x0,m)) / (x4,m4)) . x0) = (((v / (x3,m0)) / (x0,m)) . x0) by FUNCT_7: 32, ZF_LANG1: 76;

              ((((v / (x3,m0)) / (x0,m)) / (x4,m4)) . x4) = m4 by FUNCT_7: 128;

              then (M,(((v / (x3,m0)) / (x0,m)) / (x4,m4))) |= (x4 '=' x0) by A48, A44, A45, A49, A52, A47, ZF_MODEL: 12;

              then (M,(((v / (x3,m0)) / (x0,m)) / (x4,m4))) |= H1 by A51, ZF_MODEL: 19;

              then

               A53: (M,((((v / (x3,m0)) / (x0,m)) / (x4,m4)) / (x,m0))) |= H1 by A18, Th5;

              

               A54: (((v / (x3,m3)) / (x0,m0)) . x0) = m0 by FUNCT_7: 128;

              ((((v / (x3,m3)) / (x0,m0)) / (x4,m0)) . x4) = m0 by FUNCT_7: 128;

              then (M,(((v / (x3,m3)) / (x0,m0)) / (x4,m0))) |= (x4 '=' x0) by A54, A50, ZF_MODEL: 12;

              then (M,(((v / (x3,m3)) / (x0,m0)) / (x4,m0))) |= H2 by A46, ZF_MODEL: 19;

              then

               A55: (M,((((v / (x3,m3)) / (x0,m0)) / (x4,m0)) / (x0,m))) |= H2 by A21, Th9;

              

               A56: (((v / (x3,m3)) / (x0,m)) / (x4,m0)) = (((v / (x3,m3)) / (x4,m0)) / (x0,m)) by FUNCT_7: 33, ZF_LANG1: 76;

              ((((v / (x3,m3)) / (x0,m0)) / (x4,m0)) / (x0,m)) = (((v / (x3,m3)) / (x4,m0)) / (x0,m)) by Th8;

              then

               A57: (M,((((v / (x3,m3)) / (x0,m)) / (x4,m0)) / (x,m0))) |= H2 by A19, A55, A56, Th5;

              

               A58: (v9 . x) = m0 by FUNCT_7: 128;

              (v9 / (x3,m0)) = (((((v / (x3,m3)) / (x0,m)) / (x4,m4)) / (x3,m0)) / (x,m0)) by A10, FUNCT_7: 33

              .= ((((v / (x0,m)) / (x4,m4)) / (x3,m0)) / (x,m0)) by Th8

              .= ((((v / (x3,m0)) / (x0,m)) / (x4,m4)) / (x,m0)) by A20, A14, A15, Th6;

              then

               A59: (M,v9) |= (H1 / (x3,x)) by A18, A53, A58, Th12;

              (v9 / (x4,m0)) = ((((v / (x3,m3)) / (x0,m)) / (x,m0)) / (x4,m0)) by Th8

              .= ((((v / (x3,m3)) / (x0,m)) / (x4,m0)) / (x,m0)) by A16, FUNCT_7: 33;

              then (M,v9) |= (H2 / (x4,x)) by A19, A57, A58, Th12;

              then (M,v9) |= ((H1 / (x3,x)) '&' (H2 / (x4,x))) by A59, ZF_MODEL: 15;

              hence (M,(((v / (x3,m3)) / (x0,m)) / (x4,m4))) |= H by ZF_LANG1: 73;

            end;

            hence (M,(((v / (x3,m3)) / (x0,m)) / (x4,m4))) |= (H <=> (x4 '=' x0)) by A25, ZF_MODEL: 19;

          end;

          then (M,((v / (x3,m3)) / (x0,m))) |= ( All (x4,(H <=> (x4 '=' x0)))) by ZF_LANG1: 71;

          hence (M,(v / (x3,m3))) |= ( Ex (x0,( All (x4,(H <=> (x4 '=' x0)))))) by ZF_LANG1: 73;

        end;

        hence thesis by ZF_LANG1: 71;

      end;

      now

        let v;

        thus (M,v) |= H implies ((F * G) . (v . x3)) = (v . x4)

        proof

          assume (M,v) |= H;

          then

          consider m such that

           A60: (M,(v / (x,m))) |= ((H1 / (x3,x)) '&' (H2 / (x4,x))) by ZF_LANG1: 73;

          

           A61: ((v / (x,m)) . x) = m by FUNCT_7: 128;

          (M,(v / (x,m))) |= (H1 / (x3,x)) by A60, ZF_MODEL: 15;

          then (M,((v / (x,m)) / (x3,m))) |= H1 by A18, A61, Th12;

          then

           A62: (F . (((v / (x,m)) / (x3,m)) . x3)) = (((v / (x,m)) / (x3,m)) . x4) by A1, A2, A3, ZFMODEL1:def 2;

          

           A63: (((v / (x,m)) / (x3,m)) . x3) = m by FUNCT_7: 128;

          

           A64: (((v / (x,m)) / (x4,m)) . x3) = ((v / (x,m)) . x3) by FUNCT_7: 32, ZF_LANG1: 76;

          

           A65: (v . x3) = ((v / (x,m)) . x3) by A10, FUNCT_7: 32;

          

           A66: (((v / (x,m)) / (x3,m)) . x4) = ((v / (x,m)) . x4) by FUNCT_7: 32, ZF_LANG1: 76;

          (M,(v / (x,m))) |= (H2 / (x4,x)) by A60, ZF_MODEL: 15;

          then (M,((v / (x,m)) / (x4,m))) |= H2 by A19, A61, Th12;

          then

           A67: (G . (((v / (x,m)) / (x4,m)) . x3)) = (((v / (x,m)) / (x4,m)) . x4) by A4, A5, A6, ZFMODEL1:def 2;

          

           A68: (((v / (x,m)) / (x4,m)) . x4) = m by FUNCT_7: 128;

          (v . x4) = ((v / (x,m)) . x4) by A16, FUNCT_7: 32;

          hence thesis by A62, A63, A67, A68, A66, A64, A65, FUNCT_2: 15;

        end;

        set m = (G . (v . x3));

        

         A69: ((v / (x4,m)) . x4) = m by FUNCT_7: 128;

        

         A70: ((v / (x,m)) . x) = m by FUNCT_7: 128;

        

         A71: ((v / (x,m)) / (x4,m)) = ((v / (x4,m)) / (x,m)) by A16, FUNCT_7: 33;

        ((v / (x4,m)) . x3) = (v . x3) by FUNCT_7: 32, ZF_LANG1: 76;

        then (M,(v / (x4,m))) |= H2 by A4, A5, A6, A69, ZFMODEL1:def 2;

        then (M,((v / (x,m)) / (x4,m))) |= H2 by A19, A71, Th5;

        then

         A72: (M,(v / (x,m))) |= (H2 / (x4,x)) by A19, A70, Th12;

        

         A73: ((v / (x3,m)) . x3) = m by FUNCT_7: 128;

        assume ((F * G) . (v . x3)) = (v . x4);

        then

         A74: (F . m) = (v . x4) by FUNCT_2: 15;

        

         A75: ((v / (x,m)) / (x3,m)) = ((v / (x3,m)) / (x,m)) by A10, FUNCT_7: 33;

        ((v / (x3,m)) . x4) = (v . x4) by FUNCT_7: 32, ZF_LANG1: 76;

        then (M,(v / (x3,m))) |= H1 by A1, A2, A3, A74, A73, ZFMODEL1:def 2;

        then (M,((v / (x,m)) / (x3,m))) |= H1 by A18, A75, Th5;

        then (M,(v / (x,m))) |= (H1 / (x3,x)) by A18, A70, Th12;

        then (M,(v / (x,m))) |= ((H1 / (x3,x)) '&' (H2 / (x4,x))) by A72, ZF_MODEL: 15;

        hence (M,v) |= H by ZF_LANG1: 73;

      end;

      hence thesis by A11, A22, ZFMODEL1:def 2;

    end;

    theorem :: ZFMODEL2:19

    

     Th19: not ( x. 0 ) in ( Free H) implies ((M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) iff for m1 holds ex m2 st for m3 holds (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H iff m3 = m2)

    proof

      assume

       A1: not ( x. 0 ) in ( Free H);

      thus (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) implies for m1 holds ex m2 st for m3 holds (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H iff m3 = m2

      proof

        assume

         A2: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

        let m1;

        (M,(v / (( x. 3),m1))) |= ( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))) by A2, ZF_LANG1: 71;

        then

        consider m2 such that

         A3: (M,((v / (( x. 3),m1)) / (( x. 0 ),m2))) |= ( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))) by ZF_LANG1: 73;

        take m2;

        let m3;

        thus (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H implies m3 = m2

        proof

          assume (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H;

          then (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. 0 ),m2))) |= H by A1, Th9;

          then

           A4: (M,(((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3))) |= H by FUNCT_7: 33, ZF_LANG1: 76;

          (M,(((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3))) |= (H <=> (( x. 4) '=' ( x. 0 ))) by A3, ZF_LANG1: 71;

          then

           A5: (M,(((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3))) |= (( x. 4) '=' ( x. 0 )) by A4, ZF_MODEL: 19;

          

           A6: m2 = (((v / (( x. 3),m1)) / (( x. 0 ),m2)) . ( x. 0 )) by FUNCT_7: 128;

          

           A7: ((((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3)) . ( x. 0 )) = (((v / (( x. 3),m1)) / (( x. 0 ),m2)) . ( x. 0 )) by FUNCT_7: 32, ZF_LANG1: 76;

          ((((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3)) . ( x. 4)) = m3 by FUNCT_7: 128;

          hence thesis by A6, A7, A5, ZF_MODEL: 12;

        end;

        assume m3 = m2;

        then

         A8: (M,(((v / (( x. 3),m1)) / (( x. 0 ),m3)) / (( x. 4),m3))) |= (H <=> (( x. 4) '=' ( x. 0 ))) by A3, ZF_LANG1: 71;

        

         A9: ((((v / (( x. 3),m1)) / (( x. 0 ),m3)) / (( x. 4),m3)) . ( x. 0 )) = (((v / (( x. 3),m1)) / (( x. 0 ),m3)) . ( x. 0 )) by FUNCT_7: 32, ZF_LANG1: 76;

        

         A10: (((v / (( x. 3),m1)) / (( x. 0 ),m3)) . ( x. 0 )) = m3 by FUNCT_7: 128;

        ((((v / (( x. 3),m1)) / (( x. 0 ),m3)) / (( x. 4),m3)) . ( x. 4)) = m3 by FUNCT_7: 128;

        then (M,(((v / (( x. 3),m1)) / (( x. 0 ),m3)) / (( x. 4),m3))) |= (( x. 4) '=' ( x. 0 )) by A9, A10, ZF_MODEL: 12;

        then (M,(((v / (( x. 3),m1)) / (( x. 0 ),m3)) / (( x. 4),m3))) |= H by A8, ZF_MODEL: 19;

        then (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. 0 ),m3))) |= H by FUNCT_7: 33, ZF_LANG1: 76;

        hence thesis by A1, Th9;

      end;

      assume

       A11: for m1 holds ex m2 st for m3 holds (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H iff m3 = m2;

      now

        let m1;

        consider m2 such that

         A12: (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H iff m3 = m2 by A11;

        now

          let m3;

          

           A13: ((((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3)) . ( x. 0 )) = (((v / (( x. 3),m1)) / (( x. 0 ),m2)) . ( x. 0 )) by FUNCT_7: 32, ZF_LANG1: 76;

          

           A14: (((v / (( x. 3),m1)) / (( x. 0 ),m2)) . ( x. 0 )) = m2 by FUNCT_7: 128;

          

           A15: ((((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3)) . ( x. 4)) = m3 by FUNCT_7: 128;

           A16:

          now

            assume (M,(((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3))) |= (( x. 4) '=' ( x. 0 ));

            then m3 = m2 by A15, A13, A14, ZF_MODEL: 12;

            then (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H by A12;

            then (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. 0 ),m2))) |= H by A1, Th9;

            hence (M,(((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3))) |= H by FUNCT_7: 33, ZF_LANG1: 76;

          end;

          now

            assume (M,(((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3))) |= H;

            then (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. 0 ),m2))) |= H by FUNCT_7: 33, ZF_LANG1: 76;

            then (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H by A1, Th9;

            then m3 = m2 by A12;

            hence (M,(((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3))) |= (( x. 4) '=' ( x. 0 )) by A15, A13, A14, ZF_MODEL: 12;

          end;

          hence (M,(((v / (( x. 3),m1)) / (( x. 0 ),m2)) / (( x. 4),m3))) |= (H <=> (( x. 4) '=' ( x. 0 ))) by A16, ZF_MODEL: 19;

        end;

        then (M,((v / (( x. 3),m1)) / (( x. 0 ),m2))) |= ( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))) by ZF_LANG1: 71;

        hence (M,(v / (( x. 3),m1))) |= ( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))) by ZF_LANG1: 73;

      end;

      hence thesis by ZF_LANG1: 71;

    end;

    theorem :: ZFMODEL2:20

    F is_definable_in M & G is_definable_in M & ( Free H) c= {( x. 3)} implies for FG be Function st ( dom FG) = M & for v 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

    proof

      

       A1: {( x. 3), ( x. 3), ( x. 4)} = {( x. 3), ( x. 4)} by ENUMSET1: 30;

      

       A2: ( {( x. 3)} \/ {( x. 3), ( x. 4)}) = {( x. 3), ( x. 3), ( x. 4)} by ENUMSET1: 2;

      given H1 such that

       A3: ( Free H1) c= {( x. 3), ( x. 4)} and

       A4: M |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H1 <=> (( x. 4) '=' ( x. 0 ))))))))) and

       A5: F = ( def_func (H1,M));

      given H2 such that

       A6: ( Free H2) c= {( x. 3), ( x. 4)} and

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

       A8: G = ( def_func (H2,M));

      assume

       A9: ( Free H) c= {( x. 3)};

      then

       A10: not ( x. 4) in ( Free H) by Lm3, TARSKI:def 1;

      let FG be Function such that

       A11: ( dom FG) = M and

       A12: for v 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))));

      ( rng FG) c= M

      proof

        set v = the Function of VAR , M;

        let a be object;

        assume a in ( rng FG);

        then

        consider b be object such that

         A13: b in M and

         A14: a = (FG . b) by A11, FUNCT_1:def 3;

        reconsider b as Element of M by A13;

        

         A15: (M,(v / (( x. 3),b))) |= H or (M,(v / (( x. 3),b))) |= ( 'not' H) by ZF_MODEL: 14;

        ((v / (( x. 3),b)) . ( x. 3)) = b by FUNCT_7: 128;

        then (FG . b) = (( def_func (H1,M)) . b) or (FG . b) = (( def_func (H2,M)) . b) by A5, A8, A12, A15;

        hence thesis by A14;

      end;

      then

      reconsider f = FG as Function of M, M by A11, FUNCT_2:def 1, RELSET_1: 4;

      take I = ((H '&' H1) 'or' (( 'not' H) '&' H2));

      

       A16: ( Free ( 'not' H)) = ( Free H) by ZF_LANG1: 60;

      ( Free (H '&' H1)) = (( Free H) \/ ( Free H1)) by ZF_LANG1: 61;

      then

       A17: ( Free (H '&' H1)) c= {( x. 3), ( x. 4)} by A3, A9, A2, A1, XBOOLE_1: 13;

      

       A18: not ( x. 0 ) in ( Free H2) by A6, Lm1, Lm2, TARSKI:def 2;

      

       A19: not ( x. 0 ) in ( Free H1) by A3, Lm1, Lm2, TARSKI:def 2;

      ( Free (( 'not' H) '&' H2)) = (( Free ( 'not' H)) \/ ( Free H2)) by ZF_LANG1: 61;

      then

       A20: ( Free (( 'not' H) '&' H2)) c= {( x. 3), ( x. 4)} by A6, A9, A16, A2, A1, XBOOLE_1: 13;

      

       A21: ( Free I) = (( Free (H '&' H1)) \/ ( Free (( 'not' H) '&' H2))) by ZF_LANG1: 63;

      hence ( Free I) c= {( x. 3), ( x. 4)} by A17, A20, XBOOLE_1: 8;

      then

       A22: not ( x. 0 ) in ( Free I) by Lm1, Lm2, TARSKI:def 2;

       A23:

      now

        let v;

        now

          let m3;

          (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H1 <=> (( x. 4) '=' ( x. 0 ))))))))) by A4;

          then

          consider m1 such that

           A24: (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H1 iff m4 = m1 by A19, Th19;

          (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H2 <=> (( x. 4) '=' ( x. 0 ))))))))) by A7;

          then

          consider m2 such that

           A25: (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H2 iff m4 = m2 by A18, Th19;

           not (M,(v / (( x. 3),m3))) |= ( 'not' H) & (M,(v / (( x. 3),m3))) |= H or (M,(v / (( x. 3),m3))) |= ( 'not' H) & not (M,(v / (( x. 3),m3))) |= H by ZF_MODEL: 14;

          then

          consider m such that

           A26: not (M,(v / (( x. 3),m3))) |= ( 'not' H) & (M,(v / (( x. 3),m3))) |= H & m = m1 or (M,(v / (( x. 3),m3))) |= ( 'not' H) & m = m2 & not (M,(v / (( x. 3),m3))) |= H;

          take m;

          let m4;

          thus (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= I implies m4 = m

          proof

            assume (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= I;

            then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (H '&' H1) or (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (( 'not' H) '&' H2) by ZF_MODEL: 17;

            then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H & (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H1 or (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= ( 'not' H) & (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H2 by ZF_MODEL: 15;

            hence thesis by A10, A16, A24, A25, A26, Th9;

          end;

          assume m4 = m;

          then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H & (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H1 or (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= ( 'not' H) & (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H2 by A10, A16, A24, A25, A26, Th9;

          then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (H '&' H1) or (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (( 'not' H) '&' H2) by ZF_MODEL: 15;

          hence (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= I by ZF_MODEL: 17;

        end;

        hence (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(I <=> (( x. 4) '=' ( x. 0 ))))))))) by A22, Th19;

      end;

      hence

       A27: M |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(I <=> (( x. 4) '=' ( x. 0 )))))))));

      now

        set v = the Function of VAR , M;

        let a be Element of M;

        set m4 = (( def_func (I,M)) . a);

        

         A28: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(I <=> (( x. 4) '=' ( x. 0 ))))))))) by A23;

        ( def_func (I,M)) = ( def_func' (I,v)) by A21, A17, A20, A27, Th11, XBOOLE_1: 8;

        then (M,((v / (( x. 3),a)) / (( x. 4),m4))) |= I by A22, A28, Th10;

        then (M,((v / (( x. 3),a)) / (( x. 4),m4))) |= (H '&' H1) or (M,((v / (( x. 3),a)) / (( x. 4),m4))) |= (( 'not' H) '&' H2) by ZF_MODEL: 17;

        then (M,((v / (( x. 3),a)) / (( x. 4),m4))) |= H & (M,((v / (( x. 3),a)) / (( x. 4),m4))) |= H1 & (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H1 <=> (( x. 4) '=' ( x. 0 ))))))))) & ( def_func (H1,M)) = ( def_func' (H1,v)) or (M,((v / (( x. 3),a)) / (( x. 4),m4))) |= ( 'not' H) & (M,((v / (( x. 3),a)) / (( x. 4),m4))) |= H2 & (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H2 <=> (( x. 4) '=' ( x. 0 ))))))))) & ( def_func (H2,M)) = ( def_func' (H2,v)) by A3, A4, A6, A7, Th11, ZF_MODEL: 15;

        then

         A29: (M,(v / (( x. 3),a))) |= H & m4 = (F . a) or (M,(v / (( x. 3),a))) |= ( 'not' H) & m4 = (G . a) by A5, A8, A10, A16, A19, A18, Th9, Th10;

        ((v / (( x. 3),a)) . ( x. 3)) = a by FUNCT_7: 128;

        hence (f . a) = (( def_func (I,M)) . a) by A12, A29;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZFMODEL2:21

    F is_parametrically_definable_in M & G is_parametrically_definable_in M implies (G * F) is_parametrically_definable_in M

    proof

      given H1 be ZF-formula, v1 be Function of VAR , M such that

       A1: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H1) and

       A2: (M,v1) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H1 <=> (( x. 4) '=' ( x. 0 ))))))))) and

       A3: F = ( def_func' (H1,v1));

      given H2 be ZF-formula, v2 be Function of VAR , M such that

       A4: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H2) and

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

       A6: G = ( def_func' (H2,v2));

      reconsider F9 = F, G9 = G as Function of M, M by A3, A6;

      deffunc G( object) = (v2 . $1);

      consider i such that

       A7: for j st ( x. j) in ( variables_in H2) holds j < i by Th3;

      i > 4 or not i > 4;

      then

      consider i3 be Element of NAT such that

       A8: i > 4 & i3 = i or not i > 4 & i3 = 5;

      

       A9: ( x. 0 ) in {( x. 0 ), ( x. 1), ( x. 2)} by ENUMSET1:def 1;

      then not ( x. 0 ) in ( Free H1) by A1, XBOOLE_0: 3;

      then

      consider H3 be ZF-formula, v3 be Function of VAR , M such that

       A10: for j st j < i3 & ( x. j) in ( variables_in H3) holds j = 3 or j = 4 and

       A11: not ( x. 0 ) in ( Free H3) and

       A12: (M,v3) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H3 <=> (( x. 4) '=' ( x. 0 ))))))))) and

       A13: ( def_func' (H1,v1)) = ( def_func' (H3,v3)) by A2, Th16;

      consider k1 be Element of NAT such that

       A14: for j st ( x. j) in ( variables_in H3) holds j < k1 by Th3;

      k1 > i3 or k1 <= i3;

      then

      consider k be Element of NAT such that

       A15: k1 > i3 & k = k1 or k1 <= i3 & k = (i3 + 1);

      deffunc F( object) = (v3 . $1);

      defpred C[ object] means $1 in ( Free H3);

      take H = ( Ex (( x. k),((H3 / (( x. 4),( x. k))) '&' (H2 / (( x. 3),( x. k))))));

      consider v be Function such that

       A16: ( dom v) = VAR & for a be object st a in VAR holds ( C[a] implies (v . a) = F(a)) & ( not C[a] implies (v . a) = G(a)) from PARTFUN1:sch 1;

      ( rng v) c= M

      proof

        let b be object;

        assume b in ( rng v);

        then

        consider a be object such that

         A17: a in ( dom v) and

         A18: b = (v . a) by FUNCT_1:def 3;

        reconsider a as Variable by A16, A17;

        b = (v3 . a) or b = (v2 . a) by A16, A18;

        hence thesis;

      end;

      then

      reconsider v as Function of VAR , M by A16, FUNCT_2:def 1, RELSET_1: 4;

      take v;

      

       A19: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H3)

      proof

        

         A20: i3 > 2 by A8, XXREAL_0: 2;

        

         A21: i3 > 1 by A8, XXREAL_0: 2;

        assume {( x. 0 ), ( x. 1), ( x. 2)} meets ( Free H3);

        then

        consider a be object such that

         A22: a in {( x. 0 ), ( x. 1), ( x. 2)} and

         A23: a in ( Free H3) by XBOOLE_0: 3;

        

         A24: ( Free H3) c= ( variables_in H3) by ZF_LANG1: 151;

        a = ( x. 0 ) or a = ( x. 1) or a = ( x. 2) by A22, ENUMSET1:def 1;

        hence contradiction by A10, A21, A20, A23, A24;

      end;

       A25:

      now

        let a be object;

        assume

         A26: a in {( x. 0 ), ( x. 1), ( x. 2)};

        assume a in ( Free H);

        then

         A27: a in (( Free ((H3 / (( x. 4),( x. k))) '&' (H2 / (( x. 3),( x. k))))) \ {( x. k)}) by ZF_LANG1: 66;

        then

         A28: not a in {( x. k)} by XBOOLE_0:def 5;

        

         A29: ( Free ((H3 / (( x. 4),( x. k))) '&' (H2 / (( x. 3),( x. k))))) = (( Free (H3 / (( x. 4),( x. k)))) \/ ( Free (H2 / (( x. 3),( x. k))))) by ZF_LANG1: 61;

        a in ( Free ((H3 / (( x. 4),( x. k))) '&' (H2 / (( x. 3),( x. k))))) by A27, XBOOLE_0:def 5;

        then ( Free (H3 / (( x. 4),( x. k)))) c= ((( Free H3) \ {( x. 4)}) \/ {( x. k)}) & a in ( Free (H3 / (( x. 4),( x. k)))) or a in ( Free (H2 / (( x. 3),( x. k)))) & ( Free (H2 / (( x. 3),( x. k)))) c= ((( Free H2) \ {( x. 3)}) \/ {( x. k)}) by A29, Th1, XBOOLE_0:def 3;

        then a in (( Free H3) \ {( x. 4)}) or a in (( Free H2) \ {( x. 3)}) by A28, XBOOLE_0:def 3;

        then a in ( Free H3) or a in ( Free H2) by XBOOLE_0:def 5;

        hence contradiction by A4, A19, A26, XBOOLE_0: 3;

      end;

      hence {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) by XBOOLE_0: 3;

      ( x. 0 ) in {( x. 0 ), ( x. 1), ( x. 2)} by ENUMSET1:def 1;

      then

       A30: not ( x. 0 ) in ( Free H) by A25;

      

       A31: k <> 4 by A8, A15, NAT_1: 13;

      then

       A32: ( x. k) <> ( x. 4) by ZF_LANG1: 76;

      

       A33: i <= i3 by A8, XXREAL_0: 2;

      

       A34: not ( x. k) in ( variables_in H2)

      proof

        assume not thesis;

        then k < i by A7;

        hence contradiction by A33, A15, NAT_1: 13, XXREAL_0: 2;

      end;

      

       A35: x in ( Free H2) implies not x in ( Free H3) or x = ( x. 3) or x = ( x. 4)

      proof

        

         A36: ( Free H3) c= ( variables_in H3) by ZF_LANG1: 151;

        assume that

         A37: x in ( Free H2) and

         A38: x in ( Free H3);

        consider j such that

         A39: x = ( x. j) by ZF_LANG1: 77;

        ( Free H2) c= ( variables_in H2) by ZF_LANG1: 151;

        then j < i3 by A7, A33, A39, A37, XXREAL_0: 2;

        hence thesis by A10, A36, A39, A38;

      end;

      

       A40: k <> 3 by A8, A15, NAT_1: 13, XXREAL_0: 2;

      then

       A41: ( x. k) <> ( x. 3) by ZF_LANG1: 76;

      

       A42: not ( x. k) in ( variables_in H3)

      proof

        assume not thesis;

        then k < k1 by A14;

        hence contradiction by A15, NAT_1: 13;

      end;

      

       A43: not ( x. 0 ) in ( Free H2) by A4, A9, XBOOLE_0: 3;

      now

        let m1;

        

         A44: not ( x. 3) in ( variables_in (H2 / (( x. 3),( x. k)))) by A40, ZF_LANG1: 76, ZF_LANG1: 184;

        consider m such that

         A45: (M,((v3 / (( x. 3),m1)) / (( x. 4),m4))) |= H3 iff m4 = m by A11, A12, Th19;

         A46:

        now

          let x;

          assume

           A47: x in ( Free (H3 / (( x. 4),( x. k))));

          ( Free (H3 / (( x. 4),( x. k)))) c= ((( Free H3) \ {( x. 4)}) \/ {( x. k)}) by Th1;

          then x in (( Free H3) \ {( x. 4)}) or x in {( x. k)} by A47, XBOOLE_0:def 3;

          then x in ( Free H3) & not x in {( x. 4)} or x = ( x. k) by TARSKI:def 1, XBOOLE_0:def 5;

          then (x in ( Free H3) & ( x. 3) <> x & x <> ( x. k) or x = ( x. 4) or x = ( x. 3)) & x <> ( x. 4) or (((v / (( x. 3),m1)) / (( x. k),m)) . x) = m & (((v3 / (( x. 3),m1)) / (( x. k),m)) . x) = m by FUNCT_7: 128, TARSKI:def 1;

          then (((v / (( x. 3),m1)) / (( x. k),m)) . x) = ((v / (( x. 3),m1)) . x) & ((v / (( x. 3),m1)) . x) = (v . x) & (v . x) = (v3 . x) & (v3 . x) = ((v3 / (( x. 3),m1)) . x) & ((v3 / (( x. 3),m1)) . x) = (((v3 / (( x. 3),m1)) / (( x. k),m)) . x) or (((v / (( x. 3),m1)) / (( x. k),m)) . x) = ((v / (( x. 3),m1)) . x) & ((v / (( x. 3),m1)) . x) = m1 & m1 = ((v3 / (( x. 3),m1)) . x) & ((v3 / (( x. 3),m1)) . x) = (((v3 / (( x. 3),m1)) / (( x. k),m)) . x) or (((v / (( x. 3),m1)) / (( x. k),m)) . x) = (((v3 / (( x. 3),m1)) / (( x. k),m)) . x) by A41, A16, FUNCT_7: 32, FUNCT_7: 128;

          hence (((v / (( x. 3),m1)) / (( x. k),m)) . x) = (((v3 / (( x. 3),m1)) / (( x. k),m)) . x);

        end;

        consider r be Element of M such that

         A48: (M,((v2 / (( x. 3),m)) / (( x. 4),m4))) |= H2 iff m4 = r by A5, A43, Th19;

        take r;

        let m3;

        

         A49: (((v3 / (( x. 3),m1)) / (( x. 4),m)) . ( x. 4)) = m by FUNCT_7: 128;

        thus (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H implies m3 = r

        proof

           A50:

          now

            let x;

            assume x in ( Free H2);

            then not x in ( Free H3) & x <> ( x. 3) & x <> ( x. 4) or x = ( x. 3) or x = ( x. 4) by A35;

            then (((v / (( x. 3),m)) / (( x. 4),m3)) . x) = ((v / (( x. 3),m)) . x) & ((v / (( x. 3),m)) . x) = (v . x) & (v . x) = (v2 . x) & (v2 . x) = ((v2 / (( x. 3),m)) . x) & ((v2 / (( x. 3),m)) . x) = (((v2 / (( x. 3),m)) / (( x. 4),m3)) . x) or (((v / (( x. 3),m)) / (( x. 4),m3)) . x) = ((v / (( x. 3),m)) . x) & ((v / (( x. 3),m)) . x) = m & (((v2 / (( x. 3),m)) / (( x. 4),m3)) . x) = ((v2 / (( x. 3),m)) . x) & ((v2 / (( x. 3),m)) . x) = m or (((v / (( x. 3),m)) / (( x. 4),m3)) . x) = m3 & (((v2 / (( x. 3),m)) / (( x. 4),m3)) . x) = m3 by A16, Lm3, FUNCT_7: 32, FUNCT_7: 128;

            hence (((v / (( x. 3),m)) / (( x. 4),m3)) . x) = (((v2 / (( x. 3),m)) / (( x. 4),m3)) . x);

          end;

          assume (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H;

          then

          consider n be Element of M such that

           A51: (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n))) |= ((H3 / (( x. 4),( x. k))) '&' (H2 / (( x. 3),( x. k)))) by ZF_LANG1: 73;

           A52:

          now

            let x;

            assume

             A53: x in ( Free H3);

            

             A54: (((v / (( x. 3),m1)) / (( x. 4),n)) . ( x. 4)) = n by FUNCT_7: 128;

            

             A55: (((v3 / (( x. 3),m1)) / (( x. 4),n)) . ( x. 3)) = ((v3 / (( x. 3),m1)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

            

             A56: (((v / (( x. 3),m1)) / (( x. 4),n)) . ( x. 3)) = ((v / (( x. 3),m1)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

            

             A57: ((v / (( x. 3),m1)) . ( x. 3)) = m1 by FUNCT_7: 128;

            x = ( x. 3) or x = ( x. 4) or x <> ( x. 3) & x <> ( x. 4);

            then (((v / (( x. 3),m1)) / (( x. 4),n)) . x) = (((v3 / (( x. 3),m1)) / (( x. 4),n)) . x) or ((v / (( x. 3),m1)) . x) = (v . x) & ((v3 / (( x. 3),m1)) . x) = (v3 . x) & (((v / (( x. 3),m1)) / (( x. 4),n)) . x) = ((v / (( x. 3),m1)) . x) & (((v3 / (( x. 3),m1)) / (( x. 4),n)) . x) = ((v3 / (( x. 3),m1)) . x) by A54, A57, A56, A55, FUNCT_7: 32, FUNCT_7: 128;

            hence (((v / (( x. 3),m1)) / (( x. 4),n)) . x) = (((v3 / (( x. 3),m1)) / (( x. 4),n)) . x) by A16, A53;

          end;

          

           A58: (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n))) |= (H2 / (( x. 3),( x. k))) by A51, ZF_MODEL: 15;

          

           A59: ((((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n)) . ( x. k)) = n by FUNCT_7: 128;

          (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n))) |= (H3 / (( x. 4),( x. k))) by A51, ZF_MODEL: 15;

          then (M,((((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n)) / (( x. 4),n))) |= H3 by A42, A59, Th12;

          then (M,(((v / (( x. 3),m1)) / (( x. k),n)) / (( x. 4),n))) |= H3 by Th8;

          then (M,(((v / (( x. 3),m1)) / (( x. 4),n)) / (( x. k),n))) |= H3 by A31, FUNCT_7: 33, ZF_LANG1: 76;

          then (M,((v / (( x. 3),m1)) / (( x. 4),n))) |= H3 by A42, Th5;

          then (M,((v3 / (( x. 3),m1)) / (( x. 4),n))) |= H3 by A52, ZF_LANG1: 75;

          then n = m by A45;

          then (M,((((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),m)) / (( x. 3),m))) |= H2 by A34, A59, A58, Th12;

          then (M,(((v / (( x. 4),m3)) / (( x. k),m)) / (( x. 3),m))) |= H2 by Th8;

          then (M,(((v / (( x. 3),m)) / (( x. 4),m3)) / (( x. k),m))) |= H2 by A41, A32, Lm3, Th6;

          then (M,((v / (( x. 3),m)) / (( x. 4),m3))) |= H2 by A34, Th5;

          then (M,((v2 / (( x. 3),m)) / (( x. 4),m3))) |= H2 by A50, ZF_LANG1: 75;

          hence thesis by A48;

        end;

        assume m3 = r;

        then

         A60: (M,((v2 / (( x. 3),m)) / (( x. 4),m3))) |= H2 by A48;

        

         A61: ((v2 / (( x. 3),m)) . ( x. 3)) = m by FUNCT_7: 128;

         A62:

        now

          let x;

          assume

           A63: x in ( Free (H2 / (( x. 3),( x. k))));

          ( Free (H2 / (( x. 3),( x. k)))) c= ((( Free H2) \ {( x. 3)}) \/ {( x. k)}) by Th1;

          then x in (( Free H2) \ {( x. 3)}) or x in {( x. k)} by A63, XBOOLE_0:def 3;

          then x in ( Free H2) & not x in {( x. 3)} or x = ( x. k) by TARSKI:def 1, XBOOLE_0:def 5;

          then ( not x in ( Free H3) & ( x. 4) <> x & x <> ( x. k) or x = ( x. 3) or x = ( x. 4)) & x <> ( x. 3) or (((v / (( x. 4),m3)) / (( x. k),m)) . x) = m & (((v2 / (( x. 4),m3)) / (( x. k),m)) . x) = m by A35, FUNCT_7: 128, TARSKI:def 1;

          then (((v / (( x. 4),m3)) / (( x. k),m)) . x) = ((v / (( x. 4),m3)) . x) & ((v / (( x. 4),m3)) . x) = (v . x) & (v . x) = (v2 . x) & (v2 . x) = ((v2 / (( x. 4),m3)) . x) & ((v2 / (( x. 4),m3)) . x) = (((v2 / (( x. 4),m3)) / (( x. k),m)) . x) or (((v / (( x. 4),m3)) / (( x. k),m)) . x) = ((v / (( x. 4),m3)) . x) & ((v / (( x. 4),m3)) . x) = m3 & m3 = ((v2 / (( x. 4),m3)) . x) & ((v2 / (( x. 4),m3)) . x) = (((v2 / (( x. 4),m3)) / (( x. k),m)) . x) or (((v / (( x. 4),m3)) / (( x. k),m)) . x) = (((v2 / (( x. 4),m3)) / (( x. k),m)) . x) by A32, A16, FUNCT_7: 32, FUNCT_7: 128;

          hence (((v / (( x. 4),m3)) / (( x. k),m)) . x) = (((v2 / (( x. 4),m3)) / (( x. k),m)) . x);

        end;

        

         A64: not ( x. 4) in ( variables_in (H3 / (( x. 4),( x. k)))) by A31, ZF_LANG1: 76, ZF_LANG1: 184;

        (M,((v3 / (( x. 3),m1)) / (( x. 4),m))) |= H3 by A45;

        then (M,(((v3 / (( x. 3),m1)) / (( x. 4),m)) / (( x. k),m))) |= (H3 / (( x. 4),( x. k))) by A42, A49, Th13;

        then (M,(((v3 / (( x. 3),m1)) / (( x. k),m)) / (( x. 4),m))) |= (H3 / (( x. 4),( x. k))) by A31, FUNCT_7: 33, ZF_LANG1: 76;

        then (M,((v3 / (( x. 3),m1)) / (( x. k),m))) |= (H3 / (( x. 4),( x. k))) by A64, Th5;

        then (M,((v / (( x. 3),m1)) / (( x. k),m))) |= (H3 / (( x. 4),( x. k))) by A46, ZF_LANG1: 75;

        then (M,(((v / (( x. 3),m1)) / (( x. k),m)) / (( x. 4),m3))) |= (H3 / (( x. 4),( x. k))) by A64, Th5;

        then

         A65: (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),m))) |= (H3 / (( x. 4),( x. k))) by A31, FUNCT_7: 33, ZF_LANG1: 76;

        (((v2 / (( x. 3),m)) / (( x. 4),m3)) . ( x. 3)) = ((v2 / (( x. 3),m)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

        then (M,(((v2 / (( x. 3),m)) / (( x. 4),m3)) / (( x. k),m))) |= (H2 / (( x. 3),( x. k))) by A34, A61, A60, Th13;

        then (M,(((v2 / (( x. 4),m3)) / (( x. k),m)) / (( x. 3),m))) |= (H2 / (( x. 3),( x. k))) by A41, A32, Lm3, Th6;

        then (M,((v2 / (( x. 4),m3)) / (( x. k),m))) |= (H2 / (( x. 3),( x. k))) by A44, Th5;

        then (M,((v / (( x. 4),m3)) / (( x. k),m))) |= (H2 / (( x. 3),( x. k))) by A62, ZF_LANG1: 75;

        then (M,(((v / (( x. 4),m3)) / (( x. k),m)) / (( x. 3),m1))) |= (H2 / (( x. 3),( x. k))) by A44, Th5;

        then (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),m))) |= (H2 / (( x. 3),( x. k))) by A41, A32, Lm3, Th6;

        then (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),m))) |= ((H3 / (( x. 4),( x. k))) '&' (H2 / (( x. 3),( x. k)))) by A65, ZF_MODEL: 15;

        hence (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H by ZF_LANG1: 73;

      end;

      hence

       A66: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) by A30, Th19;

      now

        let a be object;

        assume a in M;

        then

        reconsider m1 = a as Element of M;

        set m3 = (( def_func' (H,v)) . m1);

        

         A67: ((G9 * F9) . m1) = (G9 . (F9 . m1)) by FUNCT_2: 15;

        (M,((v / (( x. 3),m1)) / (( x. 4),m3))) |= H by A30, A66, Th10;

        then

        consider n be Element of M such that

         A68: (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n))) |= ((H3 / (( x. 4),( x. k))) '&' (H2 / (( x. 3),( x. k)))) by ZF_LANG1: 73;

         A69:

        now

          let x;

          assume

           A70: x in ( Free H3);

          

           A71: (((v / (( x. 3),m1)) / (( x. 4),n)) . ( x. 4)) = n by FUNCT_7: 128;

          

           A72: (((v3 / (( x. 3),m1)) / (( x. 4),n)) . ( x. 3)) = ((v3 / (( x. 3),m1)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

          

           A73: (((v / (( x. 3),m1)) / (( x. 4),n)) . ( x. 3)) = ((v / (( x. 3),m1)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

          

           A74: ((v / (( x. 3),m1)) . ( x. 3)) = m1 by FUNCT_7: 128;

          x = ( x. 3) or x = ( x. 4) or x <> ( x. 3) & x <> ( x. 4);

          then (((v / (( x. 3),m1)) / (( x. 4),n)) . x) = (((v3 / (( x. 3),m1)) / (( x. 4),n)) . x) or ((v / (( x. 3),m1)) . x) = (v . x) & ((v3 / (( x. 3),m1)) . x) = (v3 . x) & (((v / (( x. 3),m1)) / (( x. 4),n)) . x) = ((v / (( x. 3),m1)) . x) & (((v3 / (( x. 3),m1)) / (( x. 4),n)) . x) = ((v3 / (( x. 3),m1)) . x) by A71, A74, A73, A72, FUNCT_7: 32, FUNCT_7: 128;

          hence (((v / (( x. 3),m1)) / (( x. 4),n)) . x) = (((v3 / (( x. 3),m1)) / (( x. 4),n)) . x) by A16, A70;

        end;

         A75:

        now

          let x;

          assume x in ( Free H2);

          then not x in ( Free H3) & x <> ( x. 3) & x <> ( x. 4) or x = ( x. 3) or x = ( x. 4) by A35;

          then (((v / (( x. 3),n)) / (( x. 4),m3)) . x) = ((v / (( x. 3),n)) . x) & ((v / (( x. 3),n)) . x) = (v . x) & (v . x) = (v2 . x) & (v2 . x) = ((v2 / (( x. 3),n)) . x) & ((v2 / (( x. 3),n)) . x) = (((v2 / (( x. 3),n)) / (( x. 4),m3)) . x) or (((v / (( x. 3),n)) / (( x. 4),m3)) . x) = ((v / (( x. 3),n)) . x) & ((v / (( x. 3),n)) . x) = n & (((v2 / (( x. 3),n)) / (( x. 4),m3)) . x) = ((v2 / (( x. 3),n)) . x) & ((v2 / (( x. 3),n)) . x) = n or (((v / (( x. 3),n)) / (( x. 4),m3)) . x) = m3 & (((v2 / (( x. 3),n)) / (( x. 4),m3)) . x) = m3 by A16, Lm3, FUNCT_7: 32, FUNCT_7: 128;

          hence (((v / (( x. 3),n)) / (( x. 4),m3)) . x) = (((v2 / (( x. 3),n)) / (( x. 4),m3)) . x);

        end;

        

         A76: ((((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n)) . ( x. k)) = n by FUNCT_7: 128;

        (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n))) |= (H2 / (( x. 3),( x. k))) by A68, ZF_MODEL: 15;

        then (M,((((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n)) / (( x. 3),n))) |= H2 by A34, A76, Th12;

        then (M,(((v / (( x. 4),m3)) / (( x. k),n)) / (( x. 3),n))) |= H2 by Th8;

        then (M,(((v / (( x. 3),n)) / (( x. 4),m3)) / (( x. k),n))) |= H2 by A41, A32, Lm3, Th6;

        then (M,((v / (( x. 3),n)) / (( x. 4),m3))) |= H2 by A34, Th5;

        then (M,((v2 / (( x. 3),n)) / (( x. 4),m3))) |= H2 by A75, ZF_LANG1: 75;

        then

         A77: (G9 . n) = m3 by A5, A6, A43, Th10;

        (M,(((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n))) |= (H3 / (( x. 4),( x. k))) by A68, ZF_MODEL: 15;

        then (M,((((v / (( x. 3),m1)) / (( x. 4),m3)) / (( x. k),n)) / (( x. 4),n))) |= H3 by A42, A76, Th12;

        then (M,(((v / (( x. 3),m1)) / (( x. k),n)) / (( x. 4),n))) |= H3 by Th8;

        then (M,(((v / (( x. 3),m1)) / (( x. 4),n)) / (( x. k),n))) |= H3 by A31, FUNCT_7: 33, ZF_LANG1: 76;

        then (M,((v / (( x. 3),m1)) / (( x. 4),n))) |= H3 by A42, Th5;

        then (M,((v3 / (( x. 3),m1)) / (( x. 4),n))) |= H3 by A69, ZF_LANG1: 75;

        hence ((G9 * F9) . a) = (( def_func' (H,v)) . a) by A3, A11, A12, A13, A77, A67, Th10;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: ZFMODEL2:22

     {( 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) implies for FG be Function st ( dom FG) = M & for 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

    proof

      assume that

       A1: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H1) and

       A2: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H1 <=> (( x. 4) '=' ( x. 0 ))))))))) and

       A3: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H2) and

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

       A5: {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free H) and

       A6: not ( x. 4) in ( Free H);

      let FG be Function such that

       A7: ( dom FG) = M and

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

      ( rng FG) c= M

      proof

        let a be object;

        assume a in ( rng FG);

        then

        consider b be object such that

         A9: b in M and

         A10: a = (FG . b) by A7, FUNCT_1:def 3;

        reconsider b as Element of M by A9;

        (M,(v / (( x. 3),b))) |= H or (M,(v / (( x. 3),b))) |= ( 'not' H) by ZF_MODEL: 14;

        then a = (( def_func' (H1,v)) . b) or a = (( def_func' (H2,v)) . b) by A8, A10;

        hence thesis;

      end;

      then

      reconsider f = FG as Function of M, M by A7, FUNCT_2:def 1, RELSET_1: 4;

      

       A11: ( x. 0 ) in {( x. 0 ), ( x. 1), ( x. 2)} by ENUMSET1:def 1;

      then

       A12: not ( x. 0 ) in ( Free H1) by A1, XBOOLE_0: 3;

      take p = ((H '&' H1) 'or' (( 'not' H) '&' H2)), v;

      

       A13: ( Free ( 'not' H)) = ( Free H) by ZF_LANG1: 60;

       A14:

      now

        let x be set;

        

         A15: ( Free (( 'not' H) '&' H2)) = (( Free ( 'not' H)) \/ ( Free H2)) by ZF_LANG1: 61;

        assume x in ( Free p);

        then x in (( Free (H '&' H1)) \/ ( Free (( 'not' H) '&' H2))) by ZF_LANG1: 63;

        then

         A16: x in ( Free (H '&' H1)) or x in ( Free (( 'not' H) '&' H2)) by XBOOLE_0:def 3;

        ( Free (H '&' H1)) = (( Free H) \/ ( Free H1)) by ZF_LANG1: 61;

        hence x in ( Free H) or x in ( Free H1) or x in ( Free H2) by A13, A16, A15, XBOOLE_0:def 3;

      end;

      now

        let a be object;

        assume that

         A17: a in {( x. 0 ), ( x. 1), ( x. 2)} and

         A18: a in ( Free p);

        a in ( Free H) or a in ( Free H1) or a in ( Free H2) by A14, A18;

        hence contradiction by A1, A3, A5, A17, XBOOLE_0: 3;

      end;

      hence {( x. 0 ), ( x. 1), ( x. 2)} misses ( Free p) by XBOOLE_0: 3;

      

       A19: not ( x. 0 ) in ( Free H2) by A3, A11, XBOOLE_0: 3;

       not ( x. 0 ) in ( Free H) by A5, A11, XBOOLE_0: 3;

      then

       A20: not ( x. 0 ) in ( Free p) by A14, A12, A19;

      now

        let m3;

        consider r1 be Element of M such that

         A21: (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H1 iff m4 = r1 by A2, A12, Th19;

        consider r2 be Element of M such that

         A22: (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H2 iff m4 = r2 by A4, A19, Th19;

        (M,(v / (( x. 3),m3))) |= H & not (M,(v / (( x. 3),m3))) |= ( 'not' H) or not (M,(v / (( x. 3),m3))) |= H & (M,(v / (( x. 3),m3))) |= ( 'not' H) by ZF_MODEL: 14;

        then

        consider r be Element of M such that

         A23: (M,(v / (( x. 3),m3))) |= H & not (M,(v / (( x. 3),m3))) |= ( 'not' H) & r = r1 or not (M,(v / (( x. 3),m3))) |= H & (M,(v / (( x. 3),m3))) |= ( 'not' H) & r = r2;

        take r;

        let m4;

        thus (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= p implies m4 = r

        proof

          assume (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= p;

          then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (H '&' H1) or (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (( 'not' H) '&' H2) by ZF_MODEL: 17;

          then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H & (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H1 or (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= ( 'not' H) & (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H2 by ZF_MODEL: 15;

          hence thesis by A6, A13, A21, A22, A23, Th9;

        end;

        assume m4 = r;

        then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H & (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H1 or (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= ( 'not' H) & (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= H2 by A6, A13, A21, A22, A23, Th9;

        then (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (H '&' H1) or (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= (( 'not' H) '&' H2) by ZF_MODEL: 15;

        hence (M,((v / (( x. 3),m3)) / (( x. 4),m4))) |= p by ZF_MODEL: 17;

      end;

      hence

       A24: (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(p <=> (( x. 4) '=' ( x. 0 ))))))))) by A20, Th19;

      now

        let a be Element of M;

        set r = (( def_func' (p,v)) . a);

        (M,((v / (( x. 3),a)) / (( x. 4),r))) |= p by A20, A24, Th10;

        then (M,((v / (( x. 3),a)) / (( x. 4),r))) |= (H '&' H1) or (M,((v / (( x. 3),a)) / (( x. 4),r))) |= (( 'not' H) '&' H2) by ZF_MODEL: 17;

        then (M,((v / (( x. 3),a)) / (( x. 4),r))) |= H & (M,((v / (( x. 3),a)) / (( x. 4),r))) |= H1 or (M,((v / (( x. 3),a)) / (( x. 4),r))) |= ( 'not' H) & (M,((v / (( x. 3),a)) / (( x. 4),r))) |= H2 by ZF_MODEL: 15;

        then (M,(v / (( x. 3),a))) |= H & r = (( def_func' (H1,v)) . a) or (M,(v / (( x. 3),a))) |= ( 'not' H) & r = (( def_func' (H2,v)) . a) by A2, A4, A6, A13, A12, A19, Th9, Th10;

        hence (f . a) = (( def_func' (p,v)) . a) by A8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZFMODEL2:23

    

     Th23: ( id M) is_definable_in M

    proof

      take H = (( x. 3) '=' ( x. 4));

      thus

       A1: ( Free H) c= {( x. 3), ( x. 4)} by ZF_LANG1: 58;

      reconsider i = ( id M) as Function of M, M;

      now

        let v;

        now

          let m3;

          now

            let m4;

            

             A2: m3 = ((v / (( x. 3),m3)) . ( x. 3)) by FUNCT_7: 128;

            

             A3: ((((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4)) . ( x. 0 )) = (((v / (( x. 3),m3)) / (( x. 0 ),m3)) . ( x. 0 )) by FUNCT_7: 32, ZF_LANG1: 76;

            

             A4: (((v / (( x. 3),m3)) / (( x. 0 ),m3)) . ( x. 0 )) = m3 by FUNCT_7: 128;

            

             A5: (((v / (( x. 3),m3)) / (( x. 0 ),m3)) . ( x. 3)) = ((v / (( x. 3),m3)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

            

             A6: ((((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4)) . ( x. 3)) = (((v / (( x. 3),m3)) / (( x. 0 ),m3)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

             A7:

            now

              assume (M,(((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4))) |= H;

              then ((((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4)) . ( x. 3)) = ((((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4)) . ( x. 4)) by ZF_MODEL: 12;

              hence (M,(((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4))) |= (( x. 4) '=' ( x. 0 )) by A6, A2, A5, A3, A4, ZF_MODEL: 12;

            end;

            

             A8: ((((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4)) . ( x. 4)) = m4 by FUNCT_7: 128;

            now

              assume (M,(((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4))) |= (( x. 4) '=' ( x. 0 ));

              then m4 = m3 by A3, A4, A8, ZF_MODEL: 12;

              hence (M,(((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4))) |= H by A6, A2, A5, A8, ZF_MODEL: 12;

            end;

            hence (M,(((v / (( x. 3),m3)) / (( x. 0 ),m3)) / (( x. 4),m4))) |= (H <=> (( x. 4) '=' ( x. 0 ))) by A7, ZF_MODEL: 19;

          end;

          then (M,((v / (( x. 3),m3)) / (( x. 0 ),m3))) |= ( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))) by ZF_LANG1: 71;

          hence (M,(v / (( x. 3),m3))) |= ( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))) by ZF_LANG1: 73;

        end;

        hence (M,v) |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 ))))))))) by ZF_LANG1: 71;

      end;

      hence

       A9: M |= ( All (( x. 3),( Ex (( x. 0 ),( All (( x. 4),(H <=> (( x. 4) '=' ( x. 0 )))))))));

      now

        set v = the Function of VAR , M;

        let a be Element of M;

        

         A10: a = ((v / (( x. 3),a)) . ( x. 3)) by FUNCT_7: 128;

        

         A11: (((v / (( x. 3),a)) / (( x. 4),a)) . ( x. 4)) = a by FUNCT_7: 128;

        

         A12: (((v / (( x. 3),a)) / (( x. 4),a)) . ( x. 3)) = ((v / (( x. 3),a)) . ( x. 3)) by FUNCT_7: 32, ZF_LANG1: 76;

        then (M,((v / (( x. 3),a)) / (( x. 4),a))) |= H by A10, A11, ZF_MODEL: 12;

        then (( def_func (H,M)) . a) = a by A1, A9, A12, A10, A11, ZFMODEL1:def 2;

        hence (i . a) = (( def_func (H,M)) . a);

      end;

      hence ( id M) = ( def_func (H,M));

    end;

    theorem :: ZFMODEL2:24

    ( id M) is_parametrically_definable_in M by Th23, ZFMODEL1: 14;