hilbert2.miz



    begin

    reserve X,x for set;

    theorem :: HILBERT2:1

    

     Th1: for Z be set, M be ManySortedSet of Z st for x be set st x in Z holds (M . x) is ManySortedSet of x holds for f be Function st f = ( Union M) holds ( dom f) = ( union Z)

    proof

      let Z be set, M be ManySortedSet of Z such that

       A1: for x be set st x in Z holds (M . x) is ManySortedSet of x;

      let f be Function;

      assume f = ( Union M);

      then

       A2: f = ( union ( rng M)) by CARD_3:def 4;

      for x be object holds x in ( dom f) iff ex Y be set st x in Y & Y in Z

      proof

        let x be object;

        thus x in ( dom f) implies ex Y be set st x in Y & Y in Z

        proof

          assume x in ( dom f);

          then [x, (f . x)] in f by FUNCT_1:def 2;

          then

          consider g be set such that

           A3: [x, (f . x)] in g and

           A4: g in ( rng M) by A2, TARSKI:def 4;

          consider a be object such that

           A5: a in ( dom M) and

           A6: g = (M . a) by A4, FUNCT_1:def 3;

          reconsider a as set by TARSKI: 1;

          

           A7: a in Z by A5, PARTFUN1:def 2;

          then

          reconsider g as ManySortedSet of a by A1, A6;

          take ( dom g);

          thus x in ( dom g) by A3, FUNCT_1: 1;

          thus thesis by A7, PARTFUN1:def 2;

        end;

        given Y be set such that

         A8: x in Y and

         A9: Y in Z;

        reconsider g = (M . Y) as ManySortedSet of Y by A1, A9;

        Y = ( dom g) by PARTFUN1:def 2;

        then

         A10: [x, (g . x)] in g by A8, FUNCT_1: 1;

        Z = ( dom M) by PARTFUN1:def 2;

        then g in ( rng M) by A9, FUNCT_1:def 3;

        then [x, (g . x)] in f by A2, A10, TARSKI:def 4;

        hence thesis by FUNCT_1: 1;

      end;

      hence thesis by TARSKI:def 4;

    end;

    theorem :: HILBERT2:2

    

     Th2: for x,y be set, f,g be FinSequence st ( <*x*> ^ f) = ( <*y*> ^ g) holds f = g

    proof

      let x,y be set, f,g be FinSequence;

      assume

       A1: ( <*x*> ^ f) = ( <*y*> ^ g);

      

      then x = (( <*y*> ^ g) . 1) by FINSEQ_1: 41

      .= y by FINSEQ_1: 41;

      hence thesis by A1, FINSEQ_1: 33;

    end;

    theorem :: HILBERT2:3

    

     Th3: for x be object holds <*x*> is FinSequence of X implies x in X

    proof

      let x be object;

      

       A1: ( rng <*x*>) = {x} by FINSEQ_1: 38;

      assume <*x*> is FinSequence of X;

      then {x} c= X by A1, FINSEQ_1:def 4;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: HILBERT2:4

    

     Th4: for X holds for f be FinSequence of X st f <> {} holds ex g be FinSequence of X, d be Element of X st f = (g ^ <*d*>)

    proof

      let X be set, f be FinSequence of X;

      assume f <> {} ;

      then

      consider q be FinSequence, x be object such that

       A1: f = (q ^ <*x*>) by FINSEQ_1: 46;

      reconsider q as FinSequence of X by A1, FINSEQ_1: 36;

      take q;

       <*x*> is FinSequence of X by A1, FINSEQ_1: 36;

      then

      reconsider x as Element of X by Th3;

      take x;

      thus thesis by A1;

    end;

    reserve k,m,n for Element of NAT ,

p,q,r,s,r9,s9 for Element of HP-WFF ,

T1,T2 for Tree;

    theorem :: HILBERT2:5

    

     Th5: <*x*> in ( tree (T1,T2)) iff x = 0 or x = 1

    proof

      

       A1: ( len <*T1, T2*>) = 2 & ( tree (T1,T2)) = ( tree <*T1, T2*>) by FINSEQ_1: 44, TREES_3:def 17;

      thus <*x*> in ( tree (T1,T2)) implies x = 0 or x = 1

      proof

        assume <*x*> in ( tree (T1,T2));

        then

        consider n be Nat, q be FinSequence such that

         A2: n < 2 and q in ( <*T1, T2*> . (n + 1)) and

         A3: <*x*> = ( <*n*> ^ q) by A1, TREES_3:def 15;

        x = ( <*x*> . 1) by FINSEQ_1: 40

        .= n by A3, FINSEQ_1: 41;

        hence thesis by A2, NAT_1: 23;

      end;

      assume

       A4: x = 0 or x = 1;

      then

      reconsider n = x as Element of NAT ;

      ( <*T1, T2*> . (n + 1)) = T1 or ( <*T1, T2*> . (n + 1)) = T2 by A4, FINSEQ_1: 44;

      then

       A5: {} in ( <*T1, T2*> . (n + 1)) by TREES_1: 22;

       <*n*> = ( <*n*> ^ {} ) by FINSEQ_1: 34;

      hence thesis by A1, A4, A5, TREES_3:def 15;

    end;

    scheme :: HILBERT2:sch1

    InTreeInd { T() -> Tree , P[ set] } :

for f be Element of T() holds P[f]

      provided

       A1: P[( <*> NAT )]

       and

       A2: for f be Element of T() st P[f] holds for n st (f ^ <*n*>) in T() holds P[(f ^ <*n*>)];

      defpred Q[ FinSequence] means $1 in T() implies P[$1];

      

       A3: for p be FinSequence, x be object st Q[p] holds Q[(p ^ <*x*>)]

      proof

        let p be FinSequence, x be object such that

         A4: Q[p];

        assume

         A5: (p ^ <*x*>) in T();

        then

        reconsider h = (p ^ <*x*>) as FinSequence of NAT by TREES_1: 19;

        consider g be FinSequence of NAT , n such that

         A6: h = (g ^ <*n*>) by Th4;

        

         A7: g = p by A6, FINSEQ_2: 17;

        reconsider g as Element of T() by A5, A6, TREES_1: 21;

        P[g] by A4, A7;

        hence thesis by A2, A5, A6;

      end;

      

       A8: Q[ {} ] by A1;

      for p be FinSequence holds Q[p] from FINSEQ_1:sch 3( A8, A3);

      hence thesis;

    end;

    reserve T1,T2 for DecoratedTree;

    theorem :: HILBERT2:6

    

     Th6: for x be set, T1, T2 holds ((x -tree (T1,T2)) . {} ) = x

    proof

      let x be set, T1, T2;

      (x -tree (T1,T2)) = (x -tree <*T1, T2*>) by TREES_4:def 6;

      hence thesis by TREES_4:def 4;

    end;

    theorem :: HILBERT2:7

    

     Th7: ((x -tree (T1,T2)) . <* 0 *>) = (T1 . {} ) & ((x -tree (T1,T2)) . <*1*>) = (T2 . {} )

    proof

      

       A1: ( len <*T1, T2*>) = 2 by FINSEQ_1: 44;

      reconsider w = {} as Node of T1 by TREES_1: 22;

      

       A2: ( <*T1, T2*> . ( 0 + 1)) = T1 by FINSEQ_1: 44;

      

      thus ((x -tree (T1,T2)) . <* 0 *>) = ((x -tree <*T1, T2*>) . <* 0 *>) by TREES_4:def 6

      .= ((x -tree <*T1, T2*>) . ( <* 0 *> ^ w)) by FINSEQ_1: 34

      .= (T1 . {} ) by A1, A2, TREES_4: 12;

      reconsider w = {} as Node of T2 by TREES_1: 22;

      

       A3: ( <*T1, T2*> . (1 + 1)) = T2 by FINSEQ_1: 44;

      

      thus ((x -tree (T1,T2)) . <*1*>) = ((x -tree <*T1, T2*>) . <*1*>) by TREES_4:def 6

      .= ((x -tree <*T1, T2*>) . ( <*1*> ^ w)) by FINSEQ_1: 34

      .= (T2 . {} ) by A1, A3, TREES_4: 12;

    end;

    theorem :: HILBERT2:8

    

     Th8: ((x -tree (T1,T2)) | <* 0 *>) = T1 & ((x -tree (T1,T2)) | <*1*>) = T2

    proof

      

       A1: ( len <*T1, T2*>) = 2 by FINSEQ_1: 44;

      

      thus ((x -tree (T1,T2)) | <* 0 *>) = ((x -tree <*T1, T2*>) | <* 0 *>) by TREES_4:def 6

      .= ( <*T1, T2*> . ( 0 + 1)) by A1, TREES_4:def 4

      .= T1 by FINSEQ_1: 44;

      

      thus ((x -tree (T1,T2)) | <*1*>) = ((x -tree <*T1, T2*>) | <*1*>) by TREES_4:def 6

      .= ( <*T1, T2*> . (1 + 1)) by A1, TREES_4:def 4

      .= T2 by FINSEQ_1: 44;

    end;

    registration

      let x;

      let p be DTree-yielding non empty FinSequence;

      cluster (x -tree p) -> non root;

      coherence

      proof

        assume (x -tree p) is root;

        then

         A1: ( dom (x -tree p)) = ( tree {} ) by TREES_3: 52, TREES_9:def 1;

        ex q be DTree-yielding FinSequence st p = q & ( dom (x -tree p)) = ( tree ( doms q)) by TREES_4:def 4;

        then ( dom p) <> {} & ( doms p) = {} by A1, TREES_3: 50;

        hence contradiction by TREES_3: 37;

      end;

    end

    registration

      let x;

      let T1 be DecoratedTree;

      cluster (x -tree T1) -> non root;

      coherence

      proof

        (x -tree T1) = (x -tree <*T1*>) by TREES_4:def 5;

        hence thesis;

      end;

      let T2 be DecoratedTree;

      cluster (x -tree (T1,T2)) -> non root;

      coherence

      proof

        (x -tree (T1,T2)) = (x -tree <*T1, T2*>) by TREES_4:def 6;

        hence thesis;

      end;

    end

    begin

    definition

      let n;

      :: HILBERT2:def1

      func prop n -> Element of HP-WFF equals <*(3 + n)*>;

      coherence by HILBERT1:def 4;

    end

    definition

      let D be set;

      :: original: with_VERUM

      redefine

      :: HILBERT2:def2

      attr D is with_VERUM means VERUM in D;

      compatibility ;

      :: original: with_propositional_variables

      redefine

      :: HILBERT2:def3

      attr D is with_propositional_variables means for n holds ( prop n) in D;

      compatibility

      proof

        thus D is with_propositional_variables implies for n holds ( prop n) in D;

        assume

         A1: for n holds ( prop n) in D;

        let n;

        ( prop n) = <*(3 + n)*>;

        hence thesis by A1;

      end;

    end

    definition

      let D be Subset of HP-WFF ;

      :: original: with_implication

      redefine

      :: HILBERT2:def4

      attr D is with_implication means for p, q st p in D & q in D holds (p => q) in D;

      compatibility

      proof

        thus D is with_implication implies for p, q st p in D & q in D holds (p => q) in D;

        assume

         A1: for p, q st p in D & q in D holds (p => q) in D;

        let p,q be FinSequence;

        assume

         A2: p in D & q in D;

        then

        reconsider p9 = p, q9 = q as Element of HP-WFF ;

        (p9 => q9) in D by A1, A2;

        hence thesis;

      end;

      :: original: with_conjunction

      redefine

      :: HILBERT2:def5

      attr D is with_conjunction means for p, q st p in D & q in D holds (p '&' q) in D;

      compatibility

      proof

        thus D is with_conjunction implies for p, q st p in D & q in D holds (p '&' q) in D;

        assume

         A3: for p, q st p in D & q in D holds (p '&' q) in D;

        let p,q be FinSequence;

        assume

         A4: p in D & q in D;

        then

        reconsider p9 = p, q9 = q as Element of HP-WFF ;

        (p9 '&' q9) in D by A3, A4;

        hence thesis;

      end;

    end

    reserve t,t1 for FinSequence;

    definition

      let p;

      :: HILBERT2:def6

      attr p is conjunctive means

      : Def6: ex r, s st p = (r '&' s);

      :: HILBERT2:def7

      attr p is conditional means

      : Def7: ex r, s st p = (r => s);

      :: HILBERT2:def8

      attr p is simple means

      : Def8: ex n st p = ( prop n);

    end

    scheme :: HILBERT2:sch2

    HPInd { P[ set] } :

for r holds P[r]

      provided

       A1: P[ VERUM ]

       and

       A2: for n holds P[( prop n)]

       and

       A3: for r, s st P[r] & P[s] holds P[(r '&' s)] & P[(r => s)];

      set X = { p where p be Element of HP-WFF : P[p] };

      X c= HP-WFF

      proof

        let x be object;

        assume x in X;

        then ex p be Element of HP-WFF st x = p & P[p];

        hence thesis;

      end;

      then

      reconsider X as Subset of HP-WFF ;

      let r;

      

       A4: X is with_propositional_variables

      proof

        let n;

        P[( prop n)] by A2;

        hence thesis;

      end;

      

       A5: X is with_implication

      proof

        let p, q;

        assume p in X;

        then

         A6: ex x be Element of HP-WFF st p = x & P[x];

        assume q in X;

        then ex x be Element of HP-WFF st q = x & P[x];

        then P[(p => q)] by A3, A6;

        hence thesis;

      end;

      

       A7: HP-WFF c= ( NAT * ) by HILBERT1:def 5;

      

       A8: X c= ( NAT * ) by A7;

      

       A9: X is with_conjunction

      proof

        let p, q;

        assume p in X;

        then

         A10: ex x be Element of HP-WFF st p = x & P[x];

        assume q in X;

        then ex x be Element of HP-WFF st q = x & P[x];

        then P[(p '&' q)] by A3, A10;

        hence thesis;

      end;

       VERUM in X by A1;

      then X is with_VERUM;

      then HP-WFF c= X by A8, A5, A9, A4, HILBERT1:def 6;

      then r in X;

      then ex p be Element of HP-WFF st r = p & P[p];

      hence thesis;

    end;

    theorem :: HILBERT2:9

    

     Th9: p is conjunctive or p is conditional or p is simple or p = VERUM

    proof

      defpred P[ Element of HP-WFF ] means $1 is conjunctive or $1 is conditional or $1 is simple or $1 = VERUM ;

      

       A1: P[ VERUM ];

      

       A2: for n holds P[( prop n)] by Def8;

      

       A3: for r, s st P[r] & P[s] holds P[(r '&' s)] & P[(r => s)] by Def6, Def7;

      for p holds P[p] from HPInd( A1, A2, A3);

      hence thesis;

    end;

    theorem :: HILBERT2:10

    

     Th10: ( len p) >= 1

    proof

      per cases by Th9;

        suppose p is conjunctive;

        then

        consider r, s such that

         A1: p = (r '&' s);

        ( len p) = ( len ( <*2*> ^ (r ^ s))) by A1, FINSEQ_1: 32

        .= (( len <*2*>) + ( len (r ^ s))) by FINSEQ_1: 22

        .= (1 + ( len (r ^ s))) by FINSEQ_1: 39;

        hence thesis by NAT_1: 11;

      end;

        suppose p is conditional;

        then

        consider r, s such that

         A2: p = (r => s);

        ( len p) = ( len ( <*1*> ^ (r ^ s))) by A2, FINSEQ_1: 32

        .= (( len <*1*>) + ( len (r ^ s))) by FINSEQ_1: 22

        .= (1 + ( len (r ^ s))) by FINSEQ_1: 39;

        hence thesis by NAT_1: 11;

      end;

        suppose p is simple;

        then ex n st p = ( prop n);

        hence thesis by FINSEQ_1: 39;

      end;

        suppose p = VERUM ;

        hence thesis by FINSEQ_1: 39;

      end;

    end;

    theorem :: HILBERT2:11

    

     Th11: (p . 1) = 1 implies p is conditional

    proof

      assume

       A1: (p . 1) = 1;

      per cases by Th9;

        suppose p is conjunctive;

        then

        consider r, s such that

         A2: p = (r '&' s);

        p = ( <*2*> ^ (r ^ s)) by A2, FINSEQ_1: 32;

        hence thesis by A1, FINSEQ_1: 41;

      end;

        suppose p is conditional;

        hence thesis;

      end;

        suppose p is simple;

        then

        consider n such that

         A3: p = ( prop n);

        (1 + 0 ) = (1 + (2 + n)) by A1, A3, FINSEQ_1: 40;

        hence thesis;

      end;

        suppose p = VERUM ;

        hence thesis by A1, FINSEQ_1: 40;

      end;

    end;

    theorem :: HILBERT2:12

    

     Th12: (p . 1) = 2 implies p is conjunctive

    proof

      assume

       A1: (p . 1) = 2;

      per cases by Th9;

        suppose p is conjunctive;

        hence thesis;

      end;

        suppose p is conditional;

        then

        consider r, s such that

         A2: p = (r => s);

        p = ( <*1*> ^ (r ^ s)) by A2, FINSEQ_1: 32;

        hence thesis by A1, FINSEQ_1: 41;

      end;

        suppose p is simple;

        then

        consider n such that

         A3: p = ( prop n);

        (2 + 0 ) = (2 + (1 + n)) by A1, A3, FINSEQ_1: 40;

        hence thesis;

      end;

        suppose p = VERUM ;

        hence thesis by A1, FINSEQ_1: 40;

      end;

    end;

    theorem :: HILBERT2:13

    (p . 1) = (3 + n) implies p is simple

    proof

      assume

       A1: (p . 1) = (3 + n);

      per cases by Th9;

        suppose p is conjunctive;

        then

        consider r, s such that

         A2: p = (r '&' s);

        p = ( <*2*> ^ (r ^ s)) by A2, FINSEQ_1: 32;

        then (2 + 0 ) = (2 + (1 + n)) by A1, FINSEQ_1: 41;

        hence thesis;

      end;

        suppose p is conditional;

        then

        consider r, s such that

         A3: p = (r => s);

        p = ( <*1*> ^ (r ^ s)) by A3, FINSEQ_1: 32;

        then (1 + 0 ) = (1 + (2 + n)) by A1, FINSEQ_1: 41;

        hence thesis;

      end;

        suppose p is simple;

        hence thesis;

      end;

        suppose p = VERUM ;

        hence thesis by A1, FINSEQ_1: 40;

      end;

    end;

    theorem :: HILBERT2:14

    (p . 1) = 0 implies p = VERUM

    proof

      assume

       A1: (p . 1) = 0 ;

      per cases by Th9;

        suppose p is conjunctive;

        then

        consider r, s such that

         A2: p = (r '&' s);

        p = ( <*2*> ^ (r ^ s)) by A2, FINSEQ_1: 32;

        hence thesis by A1, FINSEQ_1: 41;

      end;

        suppose p is conditional;

        then

        consider r, s such that

         A3: p = (r => s);

        p = ( <*1*> ^ (r ^ s)) by A3, FINSEQ_1: 32;

        hence thesis by A1, FINSEQ_1: 41;

      end;

        suppose p is simple;

        then ex n st p = ( prop n);

        hence thesis by A1, FINSEQ_1: 40;

      end;

        suppose p = VERUM ;

        hence thesis;

      end;

    end;

    theorem :: HILBERT2:15

    

     Th15: ( len p) < ( len (p '&' q)) & ( len q) < ( len (p '&' q))

    proof

      ( len (p '&' q)) = (( len ( <*2*> ^ p)) + ( len q)) by FINSEQ_1: 22

      .= ((( len <*2*>) + ( len p)) + ( len q)) by FINSEQ_1: 22

      .= ((1 + ( len p)) + ( len q)) by FINSEQ_1: 39

      .= (1 + (( len p) + ( len q)));

      then

       A1: (( len p) + ( len q)) < ( len (p '&' q)) by XREAL_1: 29;

      ( len p) <= (( len p) + ( len q)) & ( len q) <= (( len p) + ( len q)) by NAT_1: 11;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: HILBERT2:16

    

     Th16: ( len p) < ( len (p => q)) & ( len q) < ( len (p => q))

    proof

      ( len (p => q)) = (( len ( <*1*> ^ p)) + ( len q)) by FINSEQ_1: 22

      .= ((( len <*1*>) + ( len p)) + ( len q)) by FINSEQ_1: 22

      .= ((1 + ( len p)) + ( len q)) by FINSEQ_1: 39

      .= (1 + (( len p) + ( len q)));

      then

       A1: (( len p) + ( len q)) < ( len (p => q)) by XREAL_1: 29;

      ( len p) <= (( len p) + ( len q)) & ( len q) <= (( len p) + ( len q)) by NAT_1: 11;

      hence thesis by A1, XXREAL_0: 2;

    end;

    theorem :: HILBERT2:17

    

     Th17: p = (q ^ t) implies p = q

    proof

      defpred P[ Nat] means for p, q, t st ( len p) = $1 & p = (q ^ t) holds p = q;

      

       A1: for n be Nat st for k be Nat st k < n holds P[k] holds P[n]

      proof

        let n be Nat such that

         A2: for k be Nat st k < n holds for p, q, t st ( len p) = k & p = (q ^ t) holds p = q;

        let p, q, t such that

         A3: ( len p) = n and

         A4: p = (q ^ t);

        ( len q) >= 1 by Th10;

        then

         A5: (p . 1) = (q . 1) by A4, FINSEQ_1: 64;

        per cases by Th9;

          suppose p is conjunctive;

          then

          consider r, s such that

           A6: p = (r '&' s);

          (q . 1) = (( <*2*> ^ (r ^ s)) . 1) by A5, A6, FINSEQ_1: 32

          .= 2 by FINSEQ_1: 41;

          then q is conjunctive by Th12;

          then

          consider r9, s9 such that

           A7: q = (r9 '&' s9);

          ( <*2*> ^ ((r9 ^ s9) ^ t)) = (( <*2*> ^ (r9 ^ s9)) ^ t) by FINSEQ_1: 32

          .= (( <*2*> ^ r) ^ s) by A4, A6, A7, FINSEQ_1: 32

          .= ( <*2*> ^ (r ^ s)) by FINSEQ_1: 32;

          then ((r9 ^ s9) ^ t) = (r ^ s) by Th2;

          then

           A8: (r9 ^ (s9 ^ t)) = (r ^ s) by FINSEQ_1: 32;

          now

            per cases ;

              suppose

               A9: ( len r) <= ( len r9);

              n = (( len q) + ( len t)) by A3, A4, FINSEQ_1: 22;

              then ( len q) <= n by NAT_1: 11;

              then

               A10: ( len r9) < n by A7, Th15, XXREAL_0: 2;

              ex t1 st (r ^ t1) = r9 by A8, A9, FINSEQ_1: 47;

              then r = r9 by A2, A10;

              then

               A11: (s9 ^ t) = s by A8, FINSEQ_1: 33;

              ( len s) < n by A3, A6, Th15;

              then s9 = s by A2, A11;

              then t = {} by A11, FINSEQ_1: 87;

              hence thesis by A4, FINSEQ_1: 34;

            end;

              suppose ( len r) >= ( len r9);

              then

               A12: ex t1 st (r9 ^ t1) = r by A8, FINSEQ_1: 47;

              ( len r) < n by A3, A6, Th15;

              then r = r9 by A2, A12;

              then

               A13: (s9 ^ t) = s by A8, FINSEQ_1: 33;

              ( len s) < n by A3, A6, Th15;

              then s9 = s by A2, A13;

              then t = {} by A13, FINSEQ_1: 87;

              hence thesis by A4, FINSEQ_1: 34;

            end;

          end;

          hence thesis;

        end;

          suppose p is conditional;

          then

          consider r, s such that

           A14: p = (r => s);

          (q . 1) = (( <*1*> ^ (r ^ s)) . 1) by A5, A14, FINSEQ_1: 32

          .= 1 by FINSEQ_1: 41;

          then q is conditional by Th11;

          then

          consider r9, s9 such that

           A15: q = (r9 => s9);

          ( <*1*> ^ ((r9 ^ s9) ^ t)) = (( <*1*> ^ (r9 ^ s9)) ^ t) by FINSEQ_1: 32

          .= (( <*1*> ^ r) ^ s) by A4, A14, A15, FINSEQ_1: 32

          .= ( <*1*> ^ (r ^ s)) by FINSEQ_1: 32;

          then ((r9 ^ s9) ^ t) = (r ^ s) by Th2;

          then

           A16: (r9 ^ (s9 ^ t)) = (r ^ s) by FINSEQ_1: 32;

          now

            per cases ;

              suppose

               A17: ( len r) <= ( len r9);

              n = (( len q) + ( len t)) by A3, A4, FINSEQ_1: 22;

              then ( len q) <= n by NAT_1: 11;

              then

               A18: ( len r9) < n by A15, Th16, XXREAL_0: 2;

              ex t1 st (r ^ t1) = r9 by A16, A17, FINSEQ_1: 47;

              then r = r9 by A2, A18;

              then

               A19: (s9 ^ t) = s by A16, FINSEQ_1: 33;

              ( len s) < n by A3, A14, Th16;

              then s9 = s by A2, A19;

              then t = {} by A19, FINSEQ_1: 87;

              hence thesis by A4, FINSEQ_1: 34;

            end;

              suppose ( len r) >= ( len r9);

              then

               A20: ex t1 st (r9 ^ t1) = r by A16, FINSEQ_1: 47;

              ( len r) < n by A3, A14, Th16;

              then r = r9 by A2, A20;

              then

               A21: (s9 ^ t) = s by A16, FINSEQ_1: 33;

              ( len s) < n by A3, A14, Th16;

              then s9 = s by A2, A21;

              then t = {} by A21, FINSEQ_1: 87;

              hence thesis by A4, FINSEQ_1: 34;

            end;

          end;

          hence thesis;

        end;

          suppose

           A22: p is simple;

          

           A23: q <> {} by Th10, CARD_1: 27;

          ex n st p = ( prop n) by A22;

          hence thesis by A4, A23, FINSEQ_1: 88;

        end;

          suppose

           A24: p = VERUM ;

          q <> {} by Th10, CARD_1: 27;

          hence thesis by A4, A24, FINSEQ_1: 88;

        end;

      end;

      

       A25: for n be Nat holds P[n] from NAT_1:sch 4( A1);

      ( len p) = ( len p);

      hence thesis by A25;

    end;

    theorem :: HILBERT2:18

    

     Th18: (p ^ q) = (r ^ s) implies p = r & q = s

    proof

      assume

       A1: (p ^ q) = (r ^ s);

      per cases ;

        suppose ( len p) <= ( len r);

        then ex t st (p ^ t) = r by A1, FINSEQ_1: 47;

        hence p = r by Th17;

        hence thesis by A1, FINSEQ_1: 33;

      end;

        suppose ( len p) >= ( len r);

        then ex t st (r ^ t) = p by A1, FINSEQ_1: 47;

        hence p = r by Th17;

        hence thesis by A1, FINSEQ_1: 33;

      end;

    end;

    theorem :: HILBERT2:19

    

     Th19: (p '&' q) = (r '&' s) implies p = r & s = q

    proof

      assume (p '&' q) = (r '&' s);

      

      then ( <*2*> ^ (p ^ q)) = (r '&' s) by FINSEQ_1: 32

      .= ( <*2*> ^ (r ^ s)) by FINSEQ_1: 32;

      then (p ^ q) = (r ^ s) by Th2;

      hence thesis by Th18;

    end;

    theorem :: HILBERT2:20

    

     Th20: (p => q) = (r => s) implies p = r & s = q

    proof

      assume (p => q) = (r => s);

      

      then ( <*1*> ^ (p ^ q)) = (r => s) by FINSEQ_1: 32

      .= ( <*1*> ^ (r ^ s)) by FINSEQ_1: 32;

      then (p ^ q) = (r ^ s) by Th2;

      hence thesis by Th18;

    end;

    theorem :: HILBERT2:21

    

     Th21: ( prop n) = ( prop m) implies n = m

    proof

      assume ( prop n) = ( prop m);

      then (3 + n) = (3 + m) by FINSEQ_1: 76;

      hence thesis;

    end;

    theorem :: HILBERT2:22

    

     Th22: (p '&' q) <> (r => s)

    proof

      (p '&' q) = ( <*2*> ^ (p ^ q)) by FINSEQ_1: 32;

      then (r => s) = ( <*1*> ^ (r ^ s)) & ((p '&' q) . 1) = 2 by FINSEQ_1: 32, FINSEQ_1: 41;

      hence thesis by FINSEQ_1: 41;

    end;

    theorem :: HILBERT2:23

    

     Th23: (p '&' q) <> VERUM

    proof

      (p '&' q) = ( <*2*> ^ (p ^ q)) by FINSEQ_1: 32;

      then ((p '&' q) . 1) = 2 by FINSEQ_1: 41;

      hence thesis by FINSEQ_1: 40;

    end;

    theorem :: HILBERT2:24

    

     Th24: (p '&' q) <> ( prop n)

    proof

       A1:

      now

        assume 2 = ((2 + 1) + n);

        then (2 + 0 ) = (2 + (1 + n));

        hence contradiction;

      end;

      (p '&' q) = ( <*2*> ^ (p ^ q)) by FINSEQ_1: 32;

      then ((p '&' q) . 1) = 2 by FINSEQ_1: 41;

      hence thesis by A1, FINSEQ_1: 40;

    end;

    theorem :: HILBERT2:25

    

     Th25: (p => q) <> VERUM

    proof

      (p => q) = ( <*1*> ^ (p ^ q)) by FINSEQ_1: 32;

      then ((p => q) . 1) = 1 by FINSEQ_1: 41;

      hence thesis by FINSEQ_1: 40;

    end;

    theorem :: HILBERT2:26

    

     Th26: (p => q) <> ( prop n)

    proof

       A1:

      now

        assume 1 = ((1 + 2) + n);

        then (1 + 0 ) = (1 + (2 + n));

        hence contradiction;

      end;

      (p => q) = ( <*1*> ^ (p ^ q)) by FINSEQ_1: 32;

      then ((p => q) . 1) = 1 by FINSEQ_1: 41;

      hence thesis by A1, FINSEQ_1: 40;

    end;

    theorem :: HILBERT2:27

    

     Th27: (p '&' q) <> p & (p '&' q) <> q

    proof

      ( len p) < ( len (p '&' q)) by Th15;

      hence thesis by Th15;

    end;

    theorem :: HILBERT2:28

    

     Th28: (p => q) <> p & (p => q) <> q

    proof

      ( len p) < ( len (p => q)) by Th16;

      hence thesis by Th16;

    end;

    theorem :: HILBERT2:29

    

     Th29: VERUM <> ( prop n)

    proof

      assume

       A1: not thesis;

      ( VERUM . 1) = 0 by FINSEQ_1: 40;

      hence contradiction by A1, FINSEQ_1: 40;

    end;

    begin

    scheme :: HILBERT2:sch3

    HPMSSExL { V() -> set , P( Element of NAT ) -> set , C,I[ Element of HP-WFF , Element of HP-WFF , set, set, set] } :

ex M be ManySortedSet of HP-WFF st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & for p, q holds C[p, q, (M . p), (M . q), (M . (p '&' q))] & I[p, q, (M . p), (M . q), (M . (p => q))]

      provided

       A1: for p, q holds for a,b be set holds ex c be set st C[p, q, a, b, c]

       and

       A2: for p, q holds for a,b be set holds ex d be set st I[p, q, a, b, d]

       and

       A3: for p, q holds for a,b,c,d be set st C[p, q, a, b, c] & C[p, q, a, b, d] holds c = d

       and

       A4: for p, q holds for a,b,c,d be set st I[p, q, a, b, c] & I[p, q, a, b, d] holds c = d;

      defpred P[ object, object] means ($1 = VERUM implies $2 = V()) & for n st $1 = ( prop n) holds $2 = P(n);

      set Pn = the set of all ( prop n);

      set X = { Y where Y be Subset of HP-WFF : VERUM in Y & (for n holds ( prop n) in Y) & (for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y) & ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for a,b,c be set st a = (M . p) & b = (M . q) & c = (M . (p '&' q)) holds C[p, q, a, b, c]) & for p, q st (p => q) in Y holds for a,b,c be set st a = (M . p) & b = (M . q) & c = (M . (p => q)) holds I[p, q, a, b, c] };

      

       A5: Pn c= HP-WFF

      proof

        let x be object;

        assume x in Pn;

        then ex n st x = ( prop n);

        hence thesis;

      end;

       { VERUM } c= HP-WFF by ZFMISC_1: 31;

      then

      reconsider Y0 = (Pn \/ { VERUM }) as Subset of HP-WFF by A5, XBOOLE_1: 8;

      

       A6: for x be object st x in Y0 holds ex y be object st P[x, y]

      proof

        let x be object;

        assume

         A7: x in Y0;

        per cases by A7, XBOOLE_0:def 3;

          suppose x in Pn;

          then

          consider n such that

           A8: x = ( prop n);

          take P(n);

          thus x = VERUM implies P(n) = V() by A8, Th29;

          let k;

          assume x = ( prop k);

          hence thesis by A8, Th21;

        end;

          suppose

           A9: x in { VERUM };

          take V();

          x = VERUM by A9, TARSKI:def 1;

          hence thesis by Th29;

        end;

      end;

      consider M0 be ManySortedSet of Y0 such that

       A10: for x be object st x in Y0 holds P[x, (M0 . x)] from PBOOLE:sch 3( A6);

      

       A11: for p, q holds not (p '&' q) in Y0 & not (p => q) in Y0

      proof

        let p, q;

        assume

         A12: not thesis;

        per cases by A12, XBOOLE_0:def 3;

          suppose (p '&' q) in { VERUM } or (p => q) in { VERUM };

          then (p '&' q) = VERUM or (p => q) = VERUM by TARSKI:def 1;

          hence contradiction by Th23, Th25;

        end;

          suppose (p '&' q) in Pn;

          then ex n st (p '&' q) = ( prop n);

          hence contradiction by Th24;

        end;

          suppose (p => q) in Pn;

          then ex n st (p => q) = ( prop n);

          hence contradiction by Th26;

        end;

      end;

      then

       A13: (for p, q st (p '&' q) in Y0 or (p => q) in Y0 holds p in Y0 & q in Y0) & for p, q st (p '&' q) in Y0 holds for x,y,z be set st x = (M0 . p) & y = (M0 . q) & z = (M0 . (p '&' q)) holds C[p, q, x, y, z];

      

       A14: for n holds ( prop n) in Y0

      proof

        let k;

        ( prop k) in Pn;

        hence thesis by XBOOLE_0:def 3;

      end;

      

       A15: for n holds (M0 . ( prop n)) = P(n)

      proof

        let n;

        ( prop n) in Y0 by A14;

        hence thesis by A10;

      end;

       VERUM in { VERUM } by TARSKI:def 1;

      then

       A16: VERUM in Y0 by XBOOLE_0:def 3;

      

       A17: for Z be set st Z <> {} & Z c= X & Z is c=-linear holds ( union Z) in X

      proof

        defpred P[ object, object] means ex D1 be set, M be ManySortedSet of D1 st D1 = $1 & M = $2 & (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in D1 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in D1 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z];

        let Z be set such that

         A18: Z <> {} and

         A19: Z c= X and

         A20: Z is c=-linear;

        

         A21: X c= ( bool HP-WFF )

        proof

          let x be object;

          assume x in X;

          then ex Y be Subset of HP-WFF st x = Y & VERUM in Y & (for n holds ( prop n) in Y) & (for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y) & ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z];

          hence thesis;

        end;

        then

        reconsider uZ = ( union Z) as Subset of HP-WFF by A19, EQREL_1: 61;

        consider Z0 be object such that

         A22: Z0 in Z by A18, XBOOLE_0:def 1;

        reconsider Z0 as set by TARSKI: 1;

        

         A23: for x be object st x in Z holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in Z;

          then x in X by A19;

          then

          consider Y be Subset of HP-WFF such that

           A24: Y = x and VERUM in Y and for n holds ( prop n) in Y and for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y and

           A25: ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z];

          consider M be ManySortedSet of Y such that

           A26: ((M . VERUM ) = V() & for n holds (M . ( prop n)) = P(n)) & ((for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z]) by A25;

          take M;

          thus thesis by A24, A26;

        end;

        consider MM be ManySortedSet of Z such that

         A27: for x be object st x in Z holds P[x, (MM . x)] from PBOOLE:sch 3( A23);

        ( rng MM) is functional

        proof

          let y be object;

          assume y in ( rng MM);

          then

          consider x be object such that

           A28: x in ( dom MM) and

           A29: y = (MM . x) by FUNCT_1:def 3;

          x in Z by A28, PARTFUN1:def 2;

          then P[x, y] by A27, A29;

          hence thesis;

        end;

        then

        reconsider rr = ( rng MM) as functional set;

        

         A30: for f,g be Function st f in rr & g in rr & ( dom f) c= ( dom g) holds f tolerates g

        proof

          let f,g be Function;

          assume f in rr;

          then

          consider x1 be object such that

           A31: x1 in ( dom MM) and

           A32: f = (MM . x1) by FUNCT_1:def 3;

          reconsider x1 as set by TARSKI: 1;

          

           A33: x1 in Z by A31, PARTFUN1:def 2;

          then P[x1, (MM . x1)] by A27;

          then

           A34: ex M be ManySortedSet of x1 st M = f & (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in x1 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in x1 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z] by A32;

          then

           A35: x1 = ( dom f) by PARTFUN1:def 2;

          assume g in rr;

          then

          consider x2 be object such that

           A36: x2 in ( dom MM) and

           A37: g = (MM . x2) by FUNCT_1:def 3;

          reconsider x2 as set by TARSKI: 1;

          defpred P[ Element of HP-WFF ] means $1 in x1 implies (f . $1) = (g . $1);

          assume

           A38: ( dom f) c= ( dom g);

          x2 in Z by A36, PARTFUN1:def 2;

          then P[x2, (MM . x2)] by A27;

          then

           A39: ex M be ManySortedSet of x2 st M = g & (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in x2 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in x2 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z] by A37;

          

           A40: for n holds P[( prop n)]

          proof

            let n such that ( prop n) in x1;

            

            thus (f . ( prop n)) = P(n) by A34

            .= (g . ( prop n)) by A39;

          end;

          

           A41: x1 in X by A19, A33;

          

           A42: for r, s st P[r] & P[s] holds P[(r '&' s)] & P[(r => s)]

          proof

            

             A43: (ex Y be Subset of HP-WFF st Y = x1 & VERUM in Y & (for n holds ( prop n) in Y) & (for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y) & ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z]) & x1 c= x2 by A39, A38, A35, A41, PARTFUN1:def 2;

            let r, s such that

             A44: (r in x1 implies (f . r) = (g . r)) & (s in x1 implies (f . s) = (g . s));

            thus (r '&' s) in x1 implies (f . (r '&' s)) = (g . (r '&' s))

            proof

              assume (r '&' s) in x1;

              then C[r, s, (g . r), (g . s), (f . (r '&' s))] & C[r, s, (g . r), (g . s), (g . (r '&' s))] by A34, A39, A44, A43;

              hence thesis by A3;

            end;

            thus (r => s) in x1 implies (f . (r => s)) = (g . (r => s))

            proof

              assume (r => s) in x1;

              then I[r, s, (g . r), (g . s), (f . (r => s))] & I[r, s, (g . r), (g . s), (g . (r => s))] by A34, A39, A44, A43;

              hence thesis by A4;

            end;

          end;

          let x be object;

          assume x in (( dom f) /\ ( dom g));

          then

           A45: x in x1 by A38, A35, XBOOLE_1: 28;

          

           A46: P[ VERUM ] by A34, A39;

          for p holds P[p] from HPInd( A46, A40, A42);

          hence thesis by A21, A45, A41;

        end;

        for f,g be Function st f in rr & g in rr holds f tolerates g

        proof

          let f,g be Function;

          assume

           A47: f in rr;

          then

          consider x1 be object such that

           A48: x1 in ( dom MM) and

           A49: f = (MM . x1) by FUNCT_1:def 3;

          reconsider x1 as set by TARSKI: 1;

          

           A50: x1 in Z by A48, PARTFUN1:def 2;

          then P[x1, (MM . x1)] by A27;

          then ex M be ManySortedSet of x1 st M = f & (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in x1 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in x1 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z] by A49;

          then

           A51: x1 = ( dom f) by PARTFUN1:def 2;

          assume

           A52: g in rr;

          then

          consider x2 be object such that

           A53: x2 in ( dom MM) and

           A54: g = (MM . x2) by FUNCT_1:def 3;

          reconsider x2 as set by TARSKI: 1;

          

           A55: x2 in Z by A53, PARTFUN1:def 2;

          then (x1,x2) are_c=-comparable by A20, A50, ORDINAL1:def 8;

          then

           A56: x1 c= x2 or x2 c= x1 by XBOOLE_0:def 9;

           P[x2, (MM . x2)] by A27, A55;

          then ex M be ManySortedSet of x2 st M = g & (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in x2 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in x2 holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z] by A54;

          then x2 = ( dom g) by PARTFUN1:def 2;

          hence thesis by A30, A47, A52, A51, A56;

        end;

        then ( union rr) is Function by WELLFND1: 1;

        then

        reconsider M = ( Union MM) as Function by CARD_3:def 4;

        for x be set st x in Z holds (MM . x) is ManySortedSet of x

        proof

          let x be set;

          assume x in Z;

          then P[x, (MM . x)] by A27;

          hence thesis;

        end;

        then ( dom M) = uZ by Th1;

        then

        reconsider M as ManySortedSet of uZ by PARTFUN1:def 2, RELAT_1:def 18;

        

         A57: M = ( union rr) by CARD_3:def 4;

        

         A58: for p, q st (p '&' q) in uZ holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]

        proof

          let p, q;

          assume (p '&' q) in uZ;

          then

          consider Z1 be set such that

           A59: (p '&' q) in Z1 and

           A60: Z1 in Z by TARSKI:def 4;

          Z1 in ( dom MM) by A60, PARTFUN1:def 2;

          then (MM . Z1) in rr by FUNCT_1:def 3;

          then

           A61: (MM . Z1) c= M by A57, ZFMISC_1: 74;

          let x,y,z be set;

          assume that

           A62: x = (M . p) and

           A63: y = (M . q) and

           A64: z = (M . (p '&' q));

           P[Z1, (MM . Z1)] by A27, A60;

          then

          consider MZ1 be ManySortedSet of Z1 such that

           A65: MZ1 = (MM . Z1) and (MZ1 . VERUM ) = V() and for n holds (MZ1 . ( prop n)) = P(n) and

           A66: for p, q st (p '&' q) in Z1 holds for x,y,z be set st x = (MZ1 . p) & y = (MZ1 . q) & z = (MZ1 . (p '&' q)) holds C[p, q, x, y, z] and for p, q st (p => q) in Z1 holds for x,y,z be set st x = (MZ1 . p) & y = (MZ1 . q) & z = (MZ1 . (p => q)) holds I[p, q, x, y, z];

          (p '&' q) in ( dom MZ1) by A59, PARTFUN1:def 2;

          then

           A67: z = (MZ1 . (p '&' q)) by A65, A61, A64, GRFUNC_1: 2;

          Z1 in X by A19, A60;

          then

           A68: ex Y be Subset of HP-WFF st Z1 = Y & VERUM in Y & (for n holds ( prop n) in Y) & (for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y) & ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z];

          then q in Z1 by A59;

          then q in ( dom MZ1) by PARTFUN1:def 2;

          then

           A69: y = (MZ1 . q) by A65, A61, A63, GRFUNC_1: 2;

          p in Z1 by A59, A68;

          then p in ( dom MZ1) by PARTFUN1:def 2;

          then x = (MZ1 . p) by A65, A61, A62, GRFUNC_1: 2;

          hence thesis by A59, A66, A69, A67;

        end;

        Z0 in ( dom MM) by A22, PARTFUN1:def 2;

        then (MM . Z0) in rr by FUNCT_1:def 3;

        then

         A70: (MM . Z0) c= M by A57, ZFMISC_1: 74;

         P[Z0, (MM . Z0)] by A27, A22;

        then

        consider MZ0 be ManySortedSet of Z0 such that

         A71: MZ0 = (MM . Z0) and

         A72: (MZ0 . VERUM ) = V() and

         A73: for n holds (MZ0 . ( prop n)) = P(n) and for p, q st (p '&' q) in Z0 holds for x,y,z be set st x = (MZ0 . p) & y = (MZ0 . q) & z = (MZ0 . (p '&' q)) holds C[p, q, x, y, z] and for p, q st (p => q) in Z0 holds for x,y,z be set st x = (MZ0 . p) & y = (MZ0 . q) & z = (MZ0 . (p => q)) holds I[p, q, x, y, z];

        

         A74: Y0 c= Z0

        proof

          let x be object;

          Z0 in X by A19, A22;

          then

           A75: ex Y be Subset of HP-WFF st Y = Z0 & VERUM in Y & (for n holds ( prop n) in Y) & (for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y) & ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z];

          assume

           A76: x in Y0;

          per cases by A76, XBOOLE_0:def 3;

            suppose x in { VERUM };

            hence thesis by A75, TARSKI:def 1;

          end;

            suppose x in Pn;

            then ex n st x = ( prop n);

            hence thesis by A75;

          end;

        end;

        then

         A77: Y0 c= ( dom MZ0) by PARTFUN1:def 2;

        

         A78: for n holds (M . ( prop n)) = P(n)

        proof

          let n;

          ( prop n) in Y0 by A14;

          

          hence (M . ( prop n)) = (MZ0 . ( prop n)) by A70, A71, A77, GRFUNC_1: 2

          .= P(n) by A73;

        end;

        

         A79: for p, q st (p => q) in uZ holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z]

        proof

          let p, q;

          assume (p => q) in uZ;

          then

          consider Z1 be set such that

           A80: (p => q) in Z1 and

           A81: Z1 in Z by TARSKI:def 4;

          Z1 in ( dom MM) by A81, PARTFUN1:def 2;

          then (MM . Z1) in rr by FUNCT_1:def 3;

          then

           A82: (MM . Z1) c= M by A57, ZFMISC_1: 74;

          let x,y,z be set;

          assume that

           A83: x = (M . p) and

           A84: y = (M . q) and

           A85: z = (M . (p => q));

           P[Z1, (MM . Z1)] by A27, A81;

          then

          consider MZ1 be ManySortedSet of Z1 such that

           A86: MZ1 = (MM . Z1) and (MZ1 . VERUM ) = V() and for n holds (MZ1 . ( prop n)) = P(n) and for p, q st (p '&' q) in Z1 holds for x,y,z be set st x = (MZ1 . p) & y = (MZ1 . q) & z = (MZ1 . (p '&' q)) holds C[p, q, x, y, z] and

           A87: for p, q st (p => q) in Z1 holds for x,y,z be set st x = (MZ1 . p) & y = (MZ1 . q) & z = (MZ1 . (p => q)) holds I[p, q, x, y, z];

          (p => q) in ( dom MZ1) by A80, PARTFUN1:def 2;

          then

           A88: z = (MZ1 . (p => q)) by A86, A82, A85, GRFUNC_1: 2;

          Z1 in X by A19, A81;

          then

           A89: ex Y be Subset of HP-WFF st Z1 = Y & VERUM in Y & (for n holds ( prop n) in Y) & (for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y) & ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z];

          then q in Z1 by A80;

          then q in ( dom MZ1) by PARTFUN1:def 2;

          then

           A90: y = (MZ1 . q) by A86, A82, A84, GRFUNC_1: 2;

          p in Z1 by A80, A89;

          then p in ( dom MZ1) by PARTFUN1:def 2;

          then x = (MZ1 . p) by A86, A82, A83, GRFUNC_1: 2;

          hence thesis by A80, A87, A90, A88;

        end;

        

         A91: for p, q st (p '&' q) in uZ or (p => q) in uZ holds p in uZ & q in uZ

        proof

          let p, q;

          assume

           A92: (p '&' q) in uZ or (p => q) in uZ;

          per cases by A92;

            suppose (p '&' q) in uZ;

            then

            consider Z0 be set such that

             A93: (p '&' q) in Z0 and

             A94: Z0 in Z by TARSKI:def 4;

            Z0 in X by A19, A94;

            then ex Y be Subset of HP-WFF st Z0 = Y & VERUM in Y & (for n holds ( prop n) in Y) & (for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y) & ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z];

            then p in Z0 & q in Z0 by A93;

            hence thesis by A94, TARSKI:def 4;

          end;

            suppose (p => q) in uZ;

            then

            consider Z0 be set such that

             A95: (p => q) in Z0 and

             A96: Z0 in Z by TARSKI:def 4;

            Z0 in X by A19, A96;

            then ex Y be Subset of HP-WFF st Z0 = Y & VERUM in Y & (for n holds ( prop n) in Y) & (for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y) & ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z];

            then p in Z0 & q in Z0 by A95;

            hence thesis by A96, TARSKI:def 4;

          end;

        end;

        Z0 c= uZ by A22, ZFMISC_1: 74;

        then

         A97: Y0 c= uZ by A74;

        

         A98: for n holds ( prop n) in uZ by A14, A97;

        (M . VERUM ) = V() by A16, A70, A71, A72, A77, GRFUNC_1: 2;

        hence thesis by A16, A97, A98, A91, A78, A58, A79;

      end;

      

       A99: for p, q st (p => q) in Y0 holds for x,y,z be set st x = (M0 . p) & y = (M0 . q) & z = (M0 . (p => q)) holds I[p, q, x, y, z] by A11;

      (M0 . VERUM ) = V() by A10, A16;

      then Y0 in X by A16, A14, A15, A13, A99;

      then

      consider H be set such that

       A100: H in X and

       A101: for Z be set st Z in X & Z <> H holds not H c= Z by A17, ORDERS_1: 67;

      consider Y be Subset of HP-WFF such that

       A102: Y = H and

       A103: VERUM in Y and

       A104: for n holds ( prop n) in Y and

       A105: for p, q st (p '&' q) in Y or (p => q) in Y holds p in Y & q in Y and

       A106: ex M be ManySortedSet of Y st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & (for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z]) & for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z] by A100;

      consider M be ManySortedSet of Y such that

       A107: (M . VERUM ) = V() and

       A108: for n holds (M . ( prop n)) = P(n) and

       A109: for p, q st (p '&' q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p '&' q)) holds C[p, q, x, y, z] and

       A110: for p, q st (p => q) in Y holds for x,y,z be set st x = (M . p) & y = (M . q) & z = (M . (p => q)) holds I[p, q, x, y, z] by A106;

      

       A111: Y = HP-WFF

      proof

        defpred P[ Element of HP-WFF ] means $1 in Y;

        

         A112: for n holds P[( prop n)] by A104;

        

         A113: for r, s st P[r] & P[s] holds P[(r '&' s)] & P[(r => s)]

        proof

          let r, s such that

           A114: r in Y & s in Y;

          assume

           A115: not thesis;

          per cases by A115;

            suppose

             A116: not (r '&' s) in Y;

             {(r '&' s)} c= HP-WFF by ZFMISC_1: 31;

            then

            reconsider Y9 = (Y \/ {(r '&' s)}) as Subset of HP-WFF by XBOOLE_1: 8;

            consider CMrMs be set such that

             A117: C[r, s, (M . r), (M . s), CMrMs] by A1;

            set N = (M +* ((r '&' s) .--> CMrMs));

            

             A118: ( dom ((r '&' s) .--> CMrMs)) = {(r '&' s)};

            ( dom M) = Y by PARTFUN1:def 2;

            then ( dom N) = Y9 by A118, FUNCT_4:def 1;

            then

            reconsider N as ManySortedSet of Y9 by PARTFUN1:def 2, RELAT_1:def 18;

            (r '&' s) in {(r '&' s)} by TARSKI:def 1;

            then

             A119: (r '&' s) in Y9 by XBOOLE_0:def 3;

            

             A120: for p, q st (p => q) in Y9 holds for x,y,z be set st x = (N . p) & y = (N . q) & z = (N . (p => q)) holds I[p, q, x, y, z]

            proof

              let p, q such that

               A121: (p => q) in Y9;

              (p => q) <> (r '&' s) by Th22;

              then

               A122: not (p => q) in {(r '&' s)} by TARSKI:def 1;

              then

               A123: (p => q) in Y by A121, XBOOLE_0:def 3;

              then p in Y by A105;

              then not p in {(r '&' s)} by A116, TARSKI:def 1;

              then

               A124: (N . p) = (M . p) by A118, FUNCT_4: 11;

              q in Y by A105, A123;

              then not q in {(r '&' s)} by A116, TARSKI:def 1;

              then

               A125: (N . q) = (M . q) by A118, FUNCT_4: 11;

              

               A126: (N . (p => q)) = (M . (p => q)) by A118, A122, FUNCT_4: 11;

              let x,y,z be set;

              assume x = (N . p) & y = (N . q) & z = (N . (p => q));

              hence thesis by A110, A123, A124, A125, A126;

            end;

            

             A127: for n holds (N . ( prop n)) = P(n)

            proof

              let n;

              ( prop n) <> (r '&' s) by Th24;

              then not ( prop n) in {(r '&' s)} by TARSKI:def 1;

              

              hence (N . ( prop n)) = (M . ( prop n)) by A118, FUNCT_4: 11

              .= P(n) by A108;

            end;

            

             A128: for p, q st (p '&' q) in Y9 holds for x,y,z be set st x = (N . p) & y = (N . q) & z = (N . (p '&' q)) holds C[p, q, x, y, z]

            proof

              let p, q such that

               A129: (p '&' q) in Y9;

              let x,y,z be set such that

               A130: x = (N . p) & y = (N . q) & z = (N . (p '&' q));

              per cases ;

                suppose

                 A131: (p '&' q) = (r '&' s);

                q <> (p '&' q) by Th27;

                then not q in {(r '&' s)} by A131, TARSKI:def 1;

                then

                 A132: (N . q) = (M . q) by A118, FUNCT_4: 11;

                p <> (p '&' q) by Th27;

                then not p in {(r '&' s)} by A131, TARSKI:def 1;

                then

                 A133: (N . p) = (M . p) by A118, FUNCT_4: 11;

                (p '&' q) in {(r '&' s)} by A131, TARSKI:def 1;

                then

                 A134: (N . (p '&' q)) = (((r '&' s) .--> CMrMs) . (p '&' q)) by A118, FUNCT_4: 13;

                p = r & q = s by A131, Th19;

                hence thesis by A117, A130, A133, A132, A134, FUNCOP_1: 72;

              end;

                suppose (p '&' q) <> (r '&' s);

                then

                 A135: not (p '&' q) in {(r '&' s)} by TARSKI:def 1;

                then

                 A136: (p '&' q) in Y by A129, XBOOLE_0:def 3;

                then p in Y by A105;

                then not p in {(r '&' s)} by A116, TARSKI:def 1;

                then

                 A137: (N . p) = (M . p) by A118, FUNCT_4: 11;

                q in Y by A105, A136;

                then not q in {(r '&' s)} by A116, TARSKI:def 1;

                then

                 A138: (N . q) = (M . q) by A118, FUNCT_4: 11;

                (N . (p '&' q)) = (M . (p '&' q)) by A118, A135, FUNCT_4: 11;

                hence thesis by A109, A130, A136, A137, A138;

              end;

            end;

            

             A139: Y c= Y9 by XBOOLE_1: 7;

            then

             A140: for n holds ( prop n) in Y9 by A104;

            

             A141: for p, q st (p '&' q) in Y9 or (p => q) in Y9 holds p in Y9 & q in Y9

            proof

              let p, q such that

               A142: (p '&' q) in Y9 or (p => q) in Y9;

              per cases by A142;

                suppose (p '&' q) = (r '&' s);

                then p = r & q = s by Th19;

                hence thesis by A114, A139;

              end;

                suppose that

                 A143: (p '&' q) in Y9 and

                 A144: (p '&' q) <> (r '&' s);

                 not (p '&' q) in {(r '&' s)} by A144, TARSKI:def 1;

                then (p '&' q) in Y by A143, XBOOLE_0:def 3;

                then p in Y & q in Y by A105;

                hence thesis by A139;

              end;

                suppose

                 A145: (p => q) in Y9;

                (p => q) <> (r '&' s) by Th22;

                then not (p => q) in {(r '&' s)} by TARSKI:def 1;

                then (p => q) in Y by A145, XBOOLE_0:def 3;

                then p in Y & q in Y by A105;

                hence thesis by A139;

              end;

            end;

             VERUM <> (r '&' s) by Th23;

            then not VERUM in {(r '&' s)} by TARSKI:def 1;

            then (N . VERUM ) = V() by A107, A118, FUNCT_4: 11;

            then Y9 in X by A103, A139, A140, A141, A127, A128, A120;

            hence contradiction by A101, A102, A116, A119, XBOOLE_1: 7;

          end;

            suppose

             A146: not (r => s) in Y;

             {(r => s)} c= HP-WFF by ZFMISC_1: 31;

            then

            reconsider Y9 = (Y \/ {(r => s)}) as Subset of HP-WFF by XBOOLE_1: 8;

            consider IMrMs be set such that

             A147: I[r, s, (M . r), (M . s), IMrMs] by A2;

            set N = (M +* ((r => s) .--> IMrMs));

            

             A148: ( dom ((r => s) .--> IMrMs)) = {(r => s)};

            ( dom M) = Y by PARTFUN1:def 2;

            then ( dom N) = Y9 by A148, FUNCT_4:def 1;

            then

            reconsider N as ManySortedSet of Y9 by PARTFUN1:def 2, RELAT_1:def 18;

            (r => s) in {(r => s)} by TARSKI:def 1;

            then

             A149: (r => s) in Y9 by XBOOLE_0:def 3;

            

             A150: for p, q st (p '&' q) in Y9 holds for x,y,z be set st x = (N . p) & y = (N . q) & z = (N . (p '&' q)) holds C[p, q, x, y, z]

            proof

              let p, q such that

               A151: (p '&' q) in Y9;

              (p '&' q) <> (r => s) by Th22;

              then

               A152: not (p '&' q) in {(r => s)} by TARSKI:def 1;

              then

               A153: (p '&' q) in Y by A151, XBOOLE_0:def 3;

              then p in Y by A105;

              then not p in {(r => s)} by A146, TARSKI:def 1;

              then

               A154: (N . p) = (M . p) by A148, FUNCT_4: 11;

              q in Y by A105, A153;

              then not q in {(r => s)} by A146, TARSKI:def 1;

              then

               A155: (N . q) = (M . q) by A148, FUNCT_4: 11;

              

               A156: (N . (p '&' q)) = (M . (p '&' q)) by A148, A152, FUNCT_4: 11;

              let x,y,z be set;

              assume x = (N . p) & y = (N . q) & z = (N . (p '&' q));

              hence thesis by A109, A153, A154, A155, A156;

            end;

            

             A157: for n holds (N . ( prop n)) = P(n)

            proof

              let n;

              ( prop n) <> (r => s) by Th26;

              then not ( prop n) in {(r => s)} by TARSKI:def 1;

              

              hence (N . ( prop n)) = (M . ( prop n)) by A148, FUNCT_4: 11

              .= P(n) by A108;

            end;

            

             A158: for p, q st (p => q) in Y9 holds for x,y,z be set st x = (N . p) & y = (N . q) & z = (N . (p => q)) holds I[p, q, x, y, z]

            proof

              let p, q such that

               A159: (p => q) in Y9;

              let x,y,z be set such that

               A160: x = (N . p) & y = (N . q) & z = (N . (p => q));

              per cases ;

                suppose

                 A161: (p => q) = (r => s);

                q <> (p => q) by Th28;

                then not q in {(r => s)} by A161, TARSKI:def 1;

                then

                 A162: (N . q) = (M . q) by A148, FUNCT_4: 11;

                p <> (p => q) by Th28;

                then not p in {(r => s)} by A161, TARSKI:def 1;

                then

                 A163: (N . p) = (M . p) by A148, FUNCT_4: 11;

                (p => q) in {(r => s)} by A161, TARSKI:def 1;

                then

                 A164: (N . (p => q)) = (((r => s) .--> IMrMs) . (p => q)) by A148, FUNCT_4: 13;

                p = r & q = s by A161, Th20;

                hence thesis by A147, A160, A163, A162, A164, FUNCOP_1: 72;

              end;

                suppose (p => q) <> (r => s);

                then

                 A165: not (p => q) in {(r => s)} by TARSKI:def 1;

                then

                 A166: (p => q) in Y by A159, XBOOLE_0:def 3;

                then p in Y by A105;

                then not p in {(r => s)} by A146, TARSKI:def 1;

                then

                 A167: (N . p) = (M . p) by A148, FUNCT_4: 11;

                q in Y by A105, A166;

                then not q in {(r => s)} by A146, TARSKI:def 1;

                then

                 A168: (N . q) = (M . q) by A148, FUNCT_4: 11;

                (N . (p => q)) = (M . (p => q)) by A148, A165, FUNCT_4: 11;

                hence thesis by A110, A160, A166, A167, A168;

              end;

            end;

            

             A169: Y c= Y9 by XBOOLE_1: 7;

            then

             A170: for n holds ( prop n) in Y9 by A104;

            

             A171: for p, q st (p '&' q) in Y9 or (p => q) in Y9 holds p in Y9 & q in Y9

            proof

              let p, q such that

               A172: (p '&' q) in Y9 or (p => q) in Y9;

              per cases by A172;

                suppose (p => q) = (r => s);

                then p = r & q = s by Th20;

                hence thesis by A114, A169;

              end;

                suppose that

                 A173: (p => q) in Y9 and

                 A174: (p => q) <> (r => s);

                 not (p => q) in {(r => s)} by A174, TARSKI:def 1;

                then (p => q) in Y by A173, XBOOLE_0:def 3;

                then p in Y & q in Y by A105;

                hence thesis by A169;

              end;

                suppose

                 A175: (p '&' q) in Y9;

                (p '&' q) <> (r => s) by Th22;

                then not (p '&' q) in {(r => s)} by TARSKI:def 1;

                then (p '&' q) in Y by A175, XBOOLE_0:def 3;

                then p in Y & q in Y by A105;

                hence thesis by A169;

              end;

            end;

             VERUM <> (r => s) by Th25;

            then not VERUM in {(r => s)} by TARSKI:def 1;

            then (N . VERUM ) = V() by A107, A148, FUNCT_4: 11;

            then Y9 in X by A103, A169, A170, A171, A157, A158, A150;

            hence contradiction by A101, A102, A146, A149, XBOOLE_1: 7;

          end;

        end;

        

         A176: P[ VERUM ] by A103;

        for s holds P[s] from HPInd( A176, A112, A113);

        hence thesis by SUBSET_1: 28;

      end;

      then

      reconsider M as ManySortedSet of HP-WFF ;

      take M;

      thus thesis by A107, A108, A109, A110, A111;

    end;

    scheme :: HILBERT2:sch4

    HPMSSLambda { V() -> set , P( Element of NAT ) -> set , C,I( set, set) -> set } :

ex M be ManySortedSet of HP-WFF st (M . VERUM ) = V() & (for n holds (M . ( prop n)) = P(n)) & for p, q holds (M . (p '&' q)) = C(.,.) & (M . (p => q)) = I(.,.);

      defpred I[ Element of HP-WFF , Element of HP-WFF , set, set, set] means $5 = I($3,$4);

      defpred C[ Element of HP-WFF , Element of HP-WFF , set, set, set] means $5 = C($3,$4);

      

       A1: for p, q holds for a,b be set holds ex d be set st I[p, q, a, b, d];

      

       A2: for p, q holds for a,b,c,d be set st C[p, q, a, b, c] & C[p, q, a, b, d] holds c = d;

      

       A3: for p, q holds for a,b,c,d be set st I[p, q, a, b, c] & I[p, q, a, b, d] holds c = d;

      

       A4: for p, q holds for a,b be set holds ex c be set st C[p, q, a, b, c];

      consider M be ManySortedSet of HP-WFF such that

       A5: (M . VERUM ) = V() and

       A6: for n holds (M . ( prop n)) = P(n) and

       A7: for p, q holds C[p, q, (M . p), (M . q), (M . (p '&' q))] & I[p, q, (M . p), (M . q), (M . (p => q))] from HPMSSExL( A4, A1, A2, A3);

      take M;

      thus (M . VERUM ) = V() by A5;

      thus for n holds (M . ( prop n)) = P(n) by A6;

      let p, q;

      set x = (M . p), y = (M . q);

      thus (M . (p '&' q)) = C(x,y) by A7;

      thus thesis by A7;

    end;

    begin

    definition

      :: HILBERT2:def9

      func HP-Subformulae -> ManySortedSet of HP-WFF means

      : Def9: (it . VERUM ) = ( root-tree VERUM ) & (for n holds (it . ( prop n)) = ( root-tree ( prop n))) & for p, q holds ex p9,q9 be DecoratedTree of HP-WFF st p9 = (it . p) & q9 = (it . q) & (it . (p '&' q)) = ((p '&' q) -tree (p9,q9)) & (it . (p => q)) = ((p => q) -tree (p9,q9));

      existence

      proof

        deffunc P( Element of NAT ) = ( root-tree ( prop $1));

        defpred I[ Element of HP-WFF , Element of HP-WFF , set, set, set] means ($3 is DecoratedTree of HP-WFF & $4 is DecoratedTree of HP-WFF implies ex p9,q9 be DecoratedTree of HP-WFF st p9 = $3 & q9 = $4 & $5 = (($1 => $2) -tree (p9,q9))) & ( not $3 is DecoratedTree of HP-WFF or not $4 is DecoratedTree of HP-WFF implies $5 = {} );

        defpred C[ Element of HP-WFF , Element of HP-WFF , set, set, set] means ($3 is DecoratedTree of HP-WFF & $4 is DecoratedTree of HP-WFF implies ex p9,q9 be DecoratedTree of HP-WFF st p9 = $3 & q9 = $4 & $5 = (($1 '&' $2) -tree (p9,q9))) & ( not $3 is DecoratedTree of HP-WFF or not $4 is DecoratedTree of HP-WFF implies $5 = {} );

        

         A1: for p, q holds for a,b be set holds ex c be set st C[p, q, a, b, c]

        proof

          let p, q;

          let a,b be set;

          per cases ;

            suppose that

             A2: a is DecoratedTree of HP-WFF and

             A3: b is DecoratedTree of HP-WFF ;

            reconsider q9 = b as DecoratedTree of HP-WFF by A3;

            reconsider p9 = a as DecoratedTree of HP-WFF by A2;

            take ((p '&' q) -tree (p9,q9));

            thus thesis;

          end;

            suppose not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ;

            hence thesis;

          end;

        end;

        

         A4: for p, q holds for a,b be set holds ex d be set st I[p, q, a, b, d]

        proof

          let p, q;

          let a,b be set;

          per cases ;

            suppose that

             A5: a is DecoratedTree of HP-WFF and

             A6: b is DecoratedTree of HP-WFF ;

            reconsider q9 = b as DecoratedTree of HP-WFF by A6;

            reconsider p9 = a as DecoratedTree of HP-WFF by A5;

            take ((p => q) -tree (p9,q9));

            thus thesis;

          end;

            suppose not a is DecoratedTree of HP-WFF or not b is DecoratedTree of HP-WFF ;

            hence thesis;

          end;

        end;

        

         A7: for p, q holds for a,b,c,d be set st I[p, q, a, b, c] & I[p, q, a, b, d] holds c = d;

        

         A8: for p, q holds for a,b,c,d be set st C[p, q, a, b, c] & C[p, q, a, b, d] holds c = d;

        consider M be ManySortedSet of HP-WFF such that

         A9: (M . VERUM ) = ( root-tree VERUM ) and

         A10: for n holds (M . ( prop n)) = P(n) and

         A11: for p, q holds C[p, q, (M . p), (M . q), (M . (p '&' q))] & I[p, q, (M . p), (M . q), (M . (p => q))] from HPMSSExL( A1, A4, A8, A7);

        take M;

        thus (M . VERUM ) = ( root-tree VERUM ) by A9;

        thus for n holds (M . ( prop n)) = ( root-tree ( prop n)) by A10;

        let p, q;

        

         A12: C[p, q, (M . p), (M . q), (M . (p '&' q))] & I[p, q, (M . p), (M . q), (M . (p => q))] by A11;

        defpred P[ Element of HP-WFF ] means (M . $1) is DecoratedTree of HP-WFF ;

        

         A13: for r, s st P[r] & P[s] holds P[(r '&' s)] & P[(r => s)]

        proof

          let r, s such that

           A14: (M . r) is DecoratedTree of HP-WFF & (M . s) is DecoratedTree of HP-WFF ;

           C[r, s, (M . r), (M . s), (M . (r '&' s))] by A11;

          hence (M . (r '&' s)) is DecoratedTree of HP-WFF by A14;

           I[r, s, (M . r), (M . s), (M . (r => s))] by A11;

          hence thesis by A14;

        end;

        

         A15: for n holds P[( prop n)]

        proof

          let n;

          (M . ( prop n)) = ( root-tree ( prop n)) by A10;

          hence thesis;

        end;

        

         A16: P[ VERUM ] by A9;

        for p holds P[p] from HPInd( A16, A15, A13);

        hence thesis by A12;

      end;

      uniqueness

      proof

        let M1,M2 be ManySortedSet of HP-WFF such that

         A17: (M1 . VERUM ) = ( root-tree VERUM ) and

         A18: for n holds (M1 . ( prop n)) = ( root-tree ( prop n)) and

         A19: for p, q holds ex p9,q9 be DecoratedTree of HP-WFF st p9 = (M1 . p) & q9 = (M1 . q) & (M1 . (p '&' q)) = ((p '&' q) -tree (p9,q9)) & (M1 . (p => q)) = ((p => q) -tree (p9,q9)) and

         A20: (M2 . VERUM ) = ( root-tree VERUM ) and

         A21: for n holds (M2 . ( prop n)) = ( root-tree ( prop n)) and

         A22: for p, q holds ex p9,q9 be DecoratedTree of HP-WFF st p9 = (M2 . p) & q9 = (M2 . q) & (M2 . (p '&' q)) = ((p '&' q) -tree (p9,q9)) & (M2 . (p => q)) = ((p => q) -tree (p9,q9));

        defpred P[ Element of HP-WFF ] means (M1 . $1) = (M2 . $1);

        

         A23: for n holds P[( prop n)]

        proof

          let n;

          

          thus (M1 . ( prop n)) = ( root-tree ( prop n)) by A18

          .= (M2 . ( prop n)) by A21;

        end;

        

         A24: for r, s st P[r] & P[s] holds P[(r '&' s)] & P[(r => s)]

        proof

          let r, s such that

           A25: (M1 . r) = (M2 . r) & (M1 . s) = (M2 . s);

          

           A26: (ex p9,q9 be DecoratedTree of HP-WFF st p9 = (M1 . r) & q9 = (M1 . s) & (M1 . (r '&' s)) = ((r '&' s) -tree (p9,q9)) & (M1 . (r => s)) = ((r => s) -tree (p9,q9))) & ex p9,q9 be DecoratedTree of HP-WFF st p9 = (M2 . r) & q9 = (M2 . s) & (M2 . (r '&' s)) = ((r '&' s) -tree (p9,q9)) & (M2 . (r => s)) = ((r => s) -tree (p9,q9)) by A19, A22;

          hence (M1 . (r '&' s)) = (M2 . (r '&' s)) by A25;

          thus thesis by A25, A26;

        end;

        

         A27: P[ VERUM ] by A17, A20;

        for r holds P[r] from HPInd( A27, A23, A24);

        then for r be object st r in HP-WFF holds (M1 . r) = (M2 . r);

        hence M1 = M2 by PBOOLE: 3;

      end;

    end

    definition

      let p;

      :: HILBERT2:def10

      func Subformulae p -> DecoratedTree of HP-WFF equals ( HP-Subformulae . p);

      correctness

      proof

        defpred P[ Element of HP-WFF ] means ( HP-Subformulae . $1) is DecoratedTree of HP-WFF ;

        

         A1: for n holds P[( prop n)]

        proof

          let n;

          ( HP-Subformulae . ( prop n)) = ( root-tree ( prop n)) by Def9;

          hence thesis;

        end;

        

         A2: for r, s st P[r] & P[s] holds P[(r '&' s)] & P[(r => s)]

        proof

          let r, s;

          ex p9,q9 be DecoratedTree of HP-WFF st p9 = ( HP-Subformulae . r) & q9 = ( HP-Subformulae . s) & ( HP-Subformulae . (r '&' s)) = ((r '&' s) -tree (p9,q9)) & ( HP-Subformulae . (r => s)) = ((r => s) -tree (p9,q9)) by Def9;

          hence thesis;

        end;

        

         A3: P[ VERUM ] by Def9;

        for p holds P[p] from HPInd( A3, A1, A2);

        hence thesis;

      end;

    end

    theorem :: HILBERT2:30

    

     Th30: ( Subformulae VERUM ) = ( root-tree VERUM ) by Def9;

    theorem :: HILBERT2:31

    ( Subformulae ( prop n)) = ( root-tree ( prop n)) by Def9;

    theorem :: HILBERT2:32

    

     Th32: ( Subformulae (p '&' q)) = ((p '&' q) -tree (( Subformulae p),( Subformulae q)))

    proof

      ex p9,q9 be DecoratedTree of HP-WFF st p9 = ( HP-Subformulae . p) & q9 = ( HP-Subformulae . q) & ( HP-Subformulae . (p '&' q)) = ((p '&' q) -tree (p9,q9)) & ( HP-Subformulae . (p => q)) = ((p => q) -tree (p9,q9)) by Def9;

      hence thesis;

    end;

    theorem :: HILBERT2:33

    

     Th33: ( Subformulae (p => q)) = ((p => q) -tree (( Subformulae p),( Subformulae q)))

    proof

      ex p9,q9 be DecoratedTree of HP-WFF st p9 = ( HP-Subformulae . p) & q9 = ( HP-Subformulae . q) & ( HP-Subformulae . (p '&' q)) = ((p '&' q) -tree (p9,q9)) & ( HP-Subformulae . (p => q)) = ((p => q) -tree (p9,q9)) by Def9;

      hence thesis;

    end;

    theorem :: HILBERT2:34

    

     Th34: (( Subformulae p) . {} ) = p

    proof

      per cases by Th9;

        suppose p is conjunctive;

        then

        consider r, s such that

         A1: p = (r '&' s);

        ( Subformulae p) = (p -tree (( Subformulae r),( Subformulae s))) by A1, Th32;

        hence thesis by Th6;

      end;

        suppose p is conditional;

        then

        consider r, s such that

         A2: p = (r => s);

        ( Subformulae p) = (p -tree (( Subformulae r),( Subformulae s))) by A2, Th33;

        hence thesis by Th6;

      end;

        suppose p is simple;

        then ex n st p = ( prop n);

        then ( Subformulae p) = ( root-tree p) by Def9;

        hence thesis by TREES_4: 3;

      end;

        suppose p = VERUM ;

        hence thesis by Th30, TREES_4: 3;

      end;

    end;

    theorem :: HILBERT2:35

    

     Th35: for f be Element of ( dom ( Subformulae p)) holds (( Subformulae p) | f) = ( Subformulae (( Subformulae p) . f))

    proof

      let f be Element of ( dom ( Subformulae p));

      defpred P[ FinSequence of NAT ] means ex q be Element of HP-WFF st q = (( Subformulae p) . $1) & (( Subformulae p) | $1) = ( Subformulae q);

      

       A1: for f be Element of ( dom ( Subformulae p)) st P[f qua FinSequence of NAT ] holds for n st (f ^ <*n*>) in ( dom ( Subformulae p)) holds P[(f ^ <*n*>) qua FinSequence of NAT ]

      proof

        let f be Element of ( dom ( Subformulae p));

        given q be Element of HP-WFF such that q = (( Subformulae p) . f) and

         A2: (( Subformulae p) | f) = ( Subformulae q);

        let n such that

         A3: (f ^ <*n*>) in ( dom ( Subformulae p));

        

         A4: (( Subformulae p) | (f ^ <*n*>)) = (( Subformulae q) | <*n*>) by A2, A3, TREES_9: 3;

        

         A5: (( dom ( Subformulae p)) | f) = ( dom ( Subformulae q)) by A2, TREES_2:def 10;

        then

         A6: <*n*> in ( dom ( Subformulae q)) by A3, TREES_1:def 6;

        then

         A7: (( Subformulae p) . (f ^ <*n*>)) = (( Subformulae q) . <*n*>) by A2, A5, TREES_2:def 10;

        per cases by Th9;

          suppose q is conjunctive;

          then

          consider r, s such that

           A8: q = (r '&' s);

          

           A9: ( Subformulae q) = ((r '&' s) -tree (( Subformulae r),( Subformulae s))) by A8, Th32;

          then

           A10: ( dom ( Subformulae q)) = ( tree (( dom ( Subformulae r)),( dom ( Subformulae s)))) by TREES_4: 14;

          now

            per cases by A6, A10, Th5;

              suppose

               A11: n = 0 ;

              take r;

              

              thus r = (( Subformulae r) . {} ) by Th34

              .= (( Subformulae p) . (f ^ <*n*>)) by A7, A9, A11, Th7;

              thus (( Subformulae p) | (f ^ <*n*>)) = ( Subformulae r) by A4, A9, A11, Th8;

            end;

              suppose

               A12: n = 1;

              take s;

              

              thus s = (( Subformulae s) . {} ) by Th34

              .= (( Subformulae p) . (f ^ <*n*>)) by A7, A9, A12, Th7;

              thus (( Subformulae p) | (f ^ <*n*>)) = ( Subformulae s) by A4, A9, A12, Th8;

            end;

          end;

          hence thesis;

        end;

          suppose q is conditional;

          then

          consider r, s such that

           A13: q = (r => s);

          

           A14: ( Subformulae q) = ((r => s) -tree (( Subformulae r),( Subformulae s))) by A13, Th33;

          then

           A15: ( dom ( Subformulae q)) = ( tree (( dom ( Subformulae r)),( dom ( Subformulae s)))) by TREES_4: 14;

          now

            per cases by A6, A15, Th5;

              suppose

               A16: n = 0 ;

              take r;

              

              thus r = (( Subformulae r) . {} ) by Th34

              .= (( Subformulae p) . (f ^ <*n*>)) by A7, A14, A16, Th7;

              thus (( Subformulae p) | (f ^ <*n*>)) = ( Subformulae r) by A4, A14, A16, Th8;

            end;

              suppose

               A17: n = 1;

              take s;

              

              thus s = (( Subformulae s) . {} ) by Th34

              .= (( Subformulae p) . (f ^ <*n*>)) by A7, A14, A17, Th7;

              thus (( Subformulae p) | (f ^ <*n*>)) = ( Subformulae s) by A4, A14, A17, Th8;

            end;

          end;

          hence thesis;

        end;

          suppose q is simple;

          then

          consider k such that

           A18: q = ( prop k);

          ( Subformulae q) = ( root-tree ( prop k)) by A18, Def9;

          then ( dom ( Subformulae q)) = { {} } by TREES_1: 29, TREES_4: 3;

          hence thesis by A6, TARSKI:def 1;

        end;

          suppose q = VERUM ;

          then ( dom ( Subformulae q)) = { {} } by Th30, TREES_1: 29, TREES_4: 3;

          hence thesis by A6, TARSKI:def 1;

        end;

      end;

      (( Subformulae p) . {} ) = p by Th34;

      then

       A19: P[( <*> NAT ) qua FinSequence of NAT ] by TREES_9: 1;

      for f be Element of ( dom ( Subformulae p)) holds P[f qua FinSequence of NAT ] from InTreeInd( A19, A1);

      then P[f qua FinSequence of NAT ];

      hence thesis;

    end;

    theorem :: HILBERT2:36

    p in ( Leaves ( Subformulae q)) implies p = VERUM or p is simple

    proof

      assume p in ( Leaves ( Subformulae q));

      then p in (( Subformulae q) .: ( Leaves ( dom ( Subformulae q)))) by TREES_2:def 9;

      then

      consider x be object such that

       A1: x in ( dom ( Subformulae q)) and

       A2: x in ( Leaves ( dom ( Subformulae q))) and

       A3: p = (( Subformulae q) . x) by FUNCT_1:def 6;

      reconsider f = x as Element of ( dom ( Subformulae q)) by A1;

      

       A4: (( Subformulae q) | f) = ( Subformulae p) by A3, Th35;

      

       A5: not p is conditional

      proof

        assume not thesis;

        then

        consider r, s such that

         A6: p = (r => s);

        ( Subformulae p) = (p -tree (( Subformulae r),( Subformulae s))) by A6, Th33;

        hence contradiction by A2, A4, TREES_9: 6;

      end;

       not p is conjunctive

      proof

        assume not thesis;

        then

        consider r, s such that

         A7: p = (r '&' s);

        ( Subformulae p) = (p -tree (( Subformulae r),( Subformulae s))) by A7, Th32;

        hence contradiction by A2, A4, TREES_9: 6;

      end;

      hence thesis by A5, Th9;

    end;