hilbert4.miz



    begin

    set sw = (( 0 ,1) --> (1, 0 ));

    set I = ( id 1);

    reserve a,b,c,x,y,z,A,B,C,X,Y for set,

f,g for Function,

V for SetValuation,

P for Permutation of V,

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

n for Element of NAT ;

    registration

      let X, Y;

      let f be Relation of X, Y;

      reduce (( id X) * f) to f;

      reducibility

      proof

        ( dom f) c= X;

        hence (( id X) * f) = f by RELAT_1: 51;

      end;

      reduce (f * ( id Y)) to f;

      reducibility

      proof

        ( rng f) c= Y;

        hence thesis by RELAT_1: 53;

      end;

    end

    theorem :: HILBERT4:1

    

     Th4: for f,g be one-to-one Function st (f " ) = (g " ) holds f = g

    proof

      let f,g be one-to-one Function;

      ((f " ) " ) = f & ((g " ) " ) = g by FUNCT_1: 43;

      hence thesis;

    end;

    registration

      cluster involutive for Function;

      existence

      proof

        take ( id 1);

        thus thesis;

      end;

      let A;

      cluster involutive for Permutation of A;

      existence

      proof

        take ( id A);

        thus thesis;

      end;

    end

    theorem :: HILBERT4:2

    

     Th7: for f be involutive Function st ( rng f) c= ( dom f) holds (f * f) = ( id ( dom f))

    proof

      let f be involutive Function;

      assume ( rng f) c= ( dom f);

      then

       A1: ( dom (f * f)) = ( dom ( id ( dom f))) by RELAT_1: 27;

      now

        let x be object;

        assume

         A2: x in ( dom (f * f));

        

        hence ((f * f) . x) = (f . (f . x)) by FUNCT_1: 12

        .= x by A1, A2, PARTIT_2:def 2

        .= (( id ( dom f)) . x) by A1, A2, FUNCT_1: 18;

      end;

      hence thesis by A1, FUNCT_1: 2;

    end;

    theorem :: HILBERT4:3

    

     Th8: for f be Function st (f * f) = ( id ( dom f)) holds f is involutive

    proof

      let f be Function such that

       A1: (f * f) = ( id ( dom f));

      let x be set;

      assume

       A2: x in ( dom f);

      

      hence (f . (f . x)) = ((f * f) . x) by FUNCT_1: 13

      .= x by A1, A2, FUNCT_1: 18;

    end;

    theorem :: HILBERT4:4

    

     Th9: for f be involutive Function of A, A holds (f * f) = ( id A)

    proof

      let f be involutive Function of A, A;

      

       A1: ( dom f) = A by FUNCT_2: 52;

      then ( rng f) c= ( dom f);

      hence thesis by A1, Th7;

    end;

    theorem :: HILBERT4:5

    

     Th10: for f be Function of A, A st (f * f) = ( id A) holds f is involutive

    proof

      let f be Function of A, A;

      ( dom f) = A by FUNCT_2: 52;

      hence thesis by Th8;

    end;

    registration

      cluster involutive -> one-to-one for Function;

      coherence

      proof

        let f be Function;

        assume

         A1: f is involutive;

        let x1,x2 be object;

        assume x1 in ( dom f) & x2 in ( dom f);

        then (f . (f . x1)) = x1 & (f . (f . x2)) = x2 by A1, PARTIT_2:def 2;

        hence thesis;

      end;

    end

    registration

      let A;

      let f be involutive Permutation of A;

      cluster (f " ) -> involutive;

      coherence

      proof

        set h = (f " );

        (h " ) = f by FUNCT_1: 43;

        

        then ((h * h) " ) = (f * f) by FUNCT_1: 44

        .= ( id A) by Th9

        .= (( id A) " ) by FUNCT_1: 45;

        hence thesis by Th4, Th10;

      end;

    end

    registration

      let n be non zero Nat;

      cluster (( 0 ,n) --> (n, 0 )) -> without_fixpoints;

      coherence

      proof

        set f = (( 0 ,n) --> (n, 0 ));

        assume f is with_fixpoint;

        then

        consider x be object such that

         A1: x is_a_fixpoint_of f by ABIAN:def 5;

        

         A2: x in ( dom f) by A1, ABIAN:def 3;

        

         A3: (f . x) = x by A1, ABIAN:def 3;

        ( dom f) = { 0 , n} by FUNCT_4: 62;

        then x = 0 or x = n by A2, TARSKI:def 2;

        hence contradiction by A3, FUNCT_4: 63;

      end;

    end

    registration

      let n be non zero Nat, z be zero Nat;

      cluster ( fixpoints ((z,n) --> (n,z))) -> empty;

      coherence ;

    end

    registration

      let X be non empty set;

      cluster non empty involutive for Permutation of X;

      existence

      proof

        take ( id X);

        thus thesis;

      end;

    end

    registration

      let A, B;

      let f be involutive Function of A, A;

      let g be involutive Function of B, B;

      cluster [:f, g:] -> involutive;

      coherence

      proof

        let x;

        set h = [:f, g:];

        

         A1: ( dom h) = [:( dom f), ( dom g):] by FUNCT_3:def 8;

        assume x in ( dom h);

        then

        consider a,b be object such that

         A2: a in ( dom f) and

         A3: b in ( dom g) and

         A4: x = [a, b] by A1, ZFMISC_1:def 2;

        

         A5: (f . (f . a)) = a & (g . (g . b)) = b by A2, A3, PARTIT_2:def 2;

        

         A6: ( dom f) = A & ( dom g) = B by FUNCT_2: 52;

        

         A7: (f . a) in ( rng f) & (g . b) in ( rng g) by A2, A3, FUNCT_1:def 3;

        (h . (a,b)) = [(f . a), (g . b)] by A2, A3, FUNCT_3:def 8;

        

        hence (h . (h . x)) = (h . ((f . a),(g . b))) by A4

        .= x by A4, A5, A6, A7, FUNCT_3:def 8;

      end;

    end

    registration

      let A,B be non empty set;

      let f be involutive Permutation of A, g be involutive Permutation of B;

      cluster (f => g) -> involutive;

      coherence

      proof

        set h = (f => g);

        let x be Element of ( Funcs (A,B));

        

         A1: ((f " ) * (f " )) = ( id A) & (g * g) = ( id B) by Th9;

        

        thus (h . (h . x)) = (h . ((g * x) * (f " ))) by HILBERT3:def 1

        .= ((g * ((g * x) * (f " ))) * (f " )) by HILBERT3:def 1

        .= (((g * (g * x)) * (f " )) * (f " )) by RELAT_1: 36

        .= ((((g * g) * x) * (f " )) * (f " )) by RELAT_1: 36

        .= (x * ( id A)) by A1, RELAT_1: 36

        .= x;

      end;

    end

    begin

    theorem :: HILBERT4:6

    

     Th14: x is_a_fixpoint_of ( Perm (P,q)) implies (( SetVal (V,p)) --> x) is_a_fixpoint_of ( Perm (P,(p => q)))

    proof

      assume

       A1: x is_a_fixpoint_of ( Perm (P,q));

      set F = (( SetVal (V,p)) --> x);

      

       A2: ( dom ( Perm (P,(p => q)))) = ( SetVal (V,(p => q))) by FUNCT_2:def 1;

      

       A3: ( SetVal (V,(p => q))) = ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by HILBERT3: 32;

      x in ( dom ( Perm (P,q))) by A1, ABIAN:def 3;

      then

       A4: F is Function of ( SetVal (V,p)), ( SetVal (V,q)) by FUNCOP_1: 46;

      hence

       A5: F in ( dom ( Perm (P,(p => q)))) by A2, A3, FUNCT_2: 8;

      

       A6: ( Perm (P,(p => q))) = (( Perm (P,p)) => ( Perm (P,q))) by HILBERT3: 36;

      (( Perm (P,(p => q))) . F) in ( SetVal (V,(p => q))) by A5, FUNCT_2: 5;

      then

       A7: ( dom (( Perm (P,(p => q))) . F)) = ( SetVal (V,p)) by A3, FUNCT_2: 92;

      now

        let z be object such that

         A8: z in ( dom (( Perm (P,(p => q))) . F));

        ((( Perm (P,p)) => ( Perm (P,q))) . F) = ((( Perm (P,q)) * F) * (( Perm (P,p)) " )) by A4, HILBERT3:def 1;

        

        hence ((( Perm (P,(p => q))) . F) . z) = ((( Perm (P,q)) * F) . ((( Perm (P,p)) " ) . z)) by A6, A8, FUNCT_1: 12

        .= (( Perm (P,q)) . (F . ((( Perm (P,p)) " ) . z))) by A7, A8, FUNCT_2: 5, FUNCT_2: 15

        .= (( Perm (P,q)) . x) by A7, A8, FUNCT_2: 5, FUNCOP_1: 7

        .= x by A1, ABIAN:def 3;

      end;

      hence thesis by A7, FUNCOP_1: 11;

    end;

    theorem :: HILBERT4:7

    

     Lm2: ( Perm (P,q)) is with_fixpoint implies ( Perm (P,(p => q))) is with_fixpoint

    proof

      given x be object such that

       A1: x is_a_fixpoint_of ( Perm (P,q));

      reconsider xx = x as set by TARSKI: 1;

      take (( SetVal (V,p)) --> xx);

      thus thesis by A1, Th14;

    end;

    theorem :: HILBERT4:8

    

     Lm3: ( Perm (P,p)) is with_fixpoint & ( Perm (P,q)) is without_fixpoints implies ( Perm (P,(p => q))) is without_fixpoints

    proof

      given x1 be object such that

       A1: x1 is_a_fixpoint_of ( Perm (P,p));

      reconsider xx1 = x1 as set by TARSKI: 1;

      assume

       A2: for x2 be object holds not x2 is_a_fixpoint_of ( Perm (P,q));

      let x be object;

      assume

       A3: x is_a_fixpoint_of ( Perm (P,(p => q)));

      

       A4: x in ( dom ( Perm (P,(p => q)))) by A3, ABIAN:def 3;

      ( SetVal (V,(p => q))) = ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by HILBERT3: 32;

      then

      consider f be Function such that

       A5: x = f and ( dom f) = ( SetVal (V,p)) & ( rng f) c= ( SetVal (V,q)) by A4, FUNCT_2:def 2;

      (f . xx1) is_a_fixpoint_of ( Perm (P,q)) by A3, A1, A5, HILBERT3: 40;

      hence contradiction by A2;

    end;

    begin

    definition

      let X be set;

      :: HILBERT4:def1

      func ChoiceOn X -> set equals { [x, the Element of x] where x be Element of (X \ { {} }) : x in (X \ { {} }) };

      coherence ;

    end

    registration

      let X be set;

      cluster ( ChoiceOn X) -> Relation-like Function-like;

      coherence

      proof

        deffunc F( set) = the Element of $1;

        defpred P[ set] means $1 in (X \ { {} });

        { [x, F(x)] where x be Element of (X \ { {} }) : P[x] } is Function from FOMODEL0:sch 3;

        hence thesis;

      end;

    end

    

     Lm9: (a in ( dom ( ChoiceOn X)) implies (( ChoiceOn X) . a) in a) & ( dom ( ChoiceOn X)) = (X \ { {} })

    proof

      set f = ( ChoiceOn X), E = { {} }, LH = ( dom f), RH = (X \ E);

      

       A1: x in LH implies (x in RH & (f . x) in x)

      proof

        assume x in LH;

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

        then

        consider x1 be Element of RH such that

         B0: [x, (f . x)] = [x1, the Element of x1] & x1 in RH;

        

         B1: x = ( [x1, the Element of x1] `1 ) by B0

        .= x1;

        hence x in RH by B0;

         not x1 in { {} } by B0, XBOOLE_0:def 5;

        then

        reconsider xx1 = x1 as non empty set by TARSKI:def 1;

        (f . x) = ( [x1, the Element of x1] `2 ) by B0

        .= the Element of xx1;

        hence thesis by B1;

      end;

      hence a in LH implies (f . a) in a;

      for x be object holds x in LH implies x in RH by A1;

      then

       A2: LH c= RH by TARSKI:def 3;

      now

        let x be object;

        assume

         AA: x in RH;

        reconsider xx = x as set by TARSKI: 1;

         [x, the Element of xx] in f by AA;

        hence x in LH by XTUPLE_0:def 12;

      end;

      then RH c= LH by TARSKI:def 3;

      hence LH = RH by XBOOLE_0:def 10, A2;

    end;

    definition

      let f;

      :: HILBERT4:def2

      func FieldCover f -> set equals { {x, (f . x)} where x be Element of ( dom f) : x in ( dom f) };

      coherence ;

    end

    definition

      let f;

      :: HILBERT4:def3

      func SomePoints f -> set equals (( field f) \ ( rng ( ChoiceOn ( FieldCover f))));

      coherence ;

    end

    definition

      let f;

      :: HILBERT4:def4

      func OtherPoints f -> set equals ((( field f) \ ( fixpoints f)) \ ( SomePoints f));

      coherence ;

    end

    registration

      let g;

      cluster (( OtherPoints g) /\ ( SomePoints g)) -> empty;

      coherence

      proof

        set S = ( SomePoints g);

        (((( field g) \ ( fixpoints g)) \ S) /\ (S /\ S)) = {} ;

        hence thesis;

      end;

    end

    

     Lm23: f is involutive implies (f .: ( SomePoints f)) c= ( OtherPoints f)

    proof

      set F = ( FieldCover f), A1 = ( SomePoints f), A2 = ( OtherPoints f), B1 = (f .: A1), ch = ( ChoiceOn F), A = ( dom f), FP = ( fixpoints f);

      (B1 \ ( rng f)) = {} & (A2 \+\ ((( field f) \ FP) qua Subset of ( field f) /\ ( rng ch))) = {} ;

      then

       B4: B1 c= ( rng f) & A2 = ((( field f) \ FP) /\ ( rng ch)) by FOMODEL0: 29;

      assume

       B2: f is involutive;

      let y be object;

      assume

       B3: y in B1;

      then

      consider x be object such that

       B0: x in A & x in A1 & y = (f . x) by FUNCT_1:def 6;

      set X = {x, (f . x)};

      X in F & not X in { {} } by B0;

      then X in (F \ { {} }) by XBOOLE_0:def 5;

      then

       B1: X in ( dom ch) by Lm9;

      then (ch . X) in ( rng ch) & not x in ( rng ch) by B0, XBOOLE_0:def 5, FUNCT_1:def 3;

      then (ch . X) <> x & (ch . X) in X by B1, Lm9;

      then (ch . X) = y & x <> (f . x) & (f . y) = x by B0, B2, TARSKI:def 2, PARTIT_2:def 2;

      then y in ( rng ch) & not y is_a_fixpoint_of f by B1, FUNCT_1:def 3, ABIAN:def 3;

      then y in ( rng ch) & y in (( rng f) null ( dom f)) & not y in FP by FOMODEL0: 69, B3, B4;

      then y in (( field f) \ FP) & y in ( rng ch) by XBOOLE_0:def 5;

      hence y in A2 by B4, XBOOLE_0:def 4;

    end;

    

     Lm24: f is involutive implies (f .: ( OtherPoints f)) c= ( SomePoints f)

    proof

      set F = ( FieldCover f), S = ( SomePoints f), O = ( OtherPoints f), ch = ( ChoiceOn F), A = ( field f), FP = ( fixpoints f), E = { {} };

      assume

       B5: f is involutive;

      let y be object;

      assume

       B7: y in (f .: O);

      then

      consider x be object such that

       B0: x in ( dom f) & x in O & y = (f . x) by FUNCT_1:def 6;

      reconsider xx = x as set by TARSKI: 1;

      ((f .: O) \ ( rng f)) = {} ;

      then (f .: O) c= ( rng f) & (( rng f) null ( dom f)) c= A by FOMODEL0: 29;

      then

       B8: y in A by B7, TARSKI:def 3;

      (O \+\ ((A \ FP) /\ ( rng ch))) = {} ;

      then

       B66: x in ((A \ FP) /\ ( rng ch)) by B0, FOMODEL0: 29;

      consider X1 be object such that

       B1: X1 in ( dom ch) & x = (ch . X1) by B66, FUNCT_1:def 3;

      X1 in (F \ E) by B1, Lm9;

      then X1 in F;

      then

      consider x1 be Element of ( dom f) such that

       B2: X1 = {x1, (f . x1)} & x1 in ( dom f);

      

       B3: {x, (f . x)} = {x1, (f . x1)} by FOMODEL0: 70, B5, B2, B1, Lm9;

      (f . x) in ( rng ch) implies x in FP

      proof

        assume (f . x) in ( rng ch);

        then

        consider X2 be object such that

         C0: X2 in ( dom ch) & (f . x) = (ch . X2) by FUNCT_1:def 3;

        reconsider X22 = X2 as set by TARSKI: 1;

        X2 in (F \ E) by C0, Lm9;

        then X2 in F;

        then

        consider x2 be Element of ( dom f) such that

         C1: X2 = {x2, (f . x2)} & x2 in ( dom f);

        (f . x) in X22 by C0, Lm9;

        then (ch . X1) = (ch . X2) by B3, B2, C1, FOMODEL0: 71, B5, B0;

        then xx is_a_fixpoint_of f by C0, B0, B1, ABIAN:def 3;

        hence thesis by FOMODEL0: 69;

      end;

      hence y in S by B0, B8, XBOOLE_0:def 5;

    end;

    

     Lm30: f is involutive & ( rng f) c= ( dom f) implies ((f .: ( OtherPoints f)) = ( SomePoints f) & (f .: ( SomePoints f)) = ( OtherPoints f))

    proof

      assume f is involutive;

      then

      reconsider ff = f as involutive Function;

      set D = ( dom ff), C = ( rng ff), S = ( SomePoints ff), O = ( OtherPoints ff), F = ( fixpoints ff), I = ( id D);

      reconsider g = (ff * ff) as Function-like Relation-like Subset of I by FOMODEL0: 72;

      assume ( rng f) c= ( dom f);

      then

      reconsider C as Subset of D;

      C c= D & (D null C) c= ( field f);

      then

      reconsider CC = C as Subset of ( field f);

      set D2 = ( dom g);

      ( field ff) = (D null C);

      then

      reconsider SS = S, OO = O as Subset of D;

      C c= D;

      then

      reconsider SSS = SS, OOO = OO as Subset of D2 by RELAT_1: 27;

      g = (I | D2) by GRFUNC_1: 23;

      then (g | SS) = (I | (SSS null D2)) by RELAT_1: 71;

      

      then

       B0: (g .: SS) = (I .: SS)

      .= S;

      (g | OO) = ((I | D2) | OO) by GRFUNC_1: 23;

      then (g | OO) = (I | (OOO null D2)) by RELAT_1: 71;

      

      then

       B1: (g .: OO) = (I .: OO)

      .= O;

      (ff .: (ff .: S)) c= (ff .: O) by Lm23, RELAT_1: 123;

      then S c= (ff .: O) & (ff .: O) c= S by B0, Lm24, RELAT_1: 126;

      hence (f .: ( OtherPoints f)) = ( SomePoints f) by XBOOLE_0:def 10;

      (ff .: (ff .: O)) c= (ff .: S) by Lm24, RELAT_1: 123;

      then O c= (ff .: S) & (ff .: S) c= O by B1, Lm23, RELAT_1: 126;

      hence thesis by XBOOLE_0:def 10;

    end;

    

     Lm25: g is involutive & (( field g) \ ( fixpoints g)) <> {} & ( rng g) c= ( dom g) implies ( SomePoints g) <> {}

    proof

      assume g is involutive;

      then

      reconsider gg = g as involutive Function;

      set G = ( field gg), F = ( fixpoints gg), S = ( SomePoints gg), O = ( OtherPoints gg);

      assume

       B0: (( field g) \ ( fixpoints g)) <> {} ;

      then

      reconsider G as non empty set;

      reconsider X = (G \ F) as non empty Subset of G by B0;

      assume

       B2: ( rng g) c= ( dom g);

      assume ( SomePoints g) = {} ;

      then

      reconsider S as empty Subset of G;

      (X \ S) <> {} ;

      then

      reconsider O as non empty Subset of G;

      (gg .: S) = O by B2, Lm30;

      hence contradiction;

    end;

    

     Lm26: (( rng g) \ ( dom g)) = {} & g is involutive & (( field g) \ ( fixpoints g)) <> {} implies (( SomePoints g) <> {} & ( OtherPoints g) <> {} )

    proof

      assume (( rng g) \ ( dom g)) = {} ;

      then

       B0: ( rng g) c= ( dom g) by FOMODEL0: 29;

      assume

       B1: g is involutive & (( field g) \ ( fixpoints g)) <> {} ;

      hence ( SomePoints g) <> {} by Lm25, B0;

      then (g .: ( OtherPoints g)) <> {} by Lm30, B0, B1;

      hence thesis;

    end;

    begin

    definition

      let x;

      :: HILBERT4:def5

      func x tohilb -> set equals ((( id 1) +* ( [:1, ( Funcs (x, {} )):] * [:( Funcs (x, {} )), {1}:])) +* ( [: {1}, ( Funcs (x, {} )):] * [:( Funcs (x, {} )), { 0 }:]));

      coherence ;

    end

    registration

      let x;

      cluster (x tohilb ) -> Function-like Relation-like;

      coherence ;

    end

    theorem :: HILBERT4:9

    

     Lm18: x <> {} implies (x tohilb ) = ( id 1)

    proof

      assume x <> {} ;

      then

      reconsider xx = x as non empty set;

      (xx tohilb ) = ( id 1);

      hence thesis;

    end;

    theorem :: HILBERT4:10

    

     Lm17: ( {} tohilb ) = (( 0 ,1) --> (1, 0 ))

    proof

      reconsider X = ( Funcs ( {} , {} )) as non empty set;

      reconsider I = ( id 1) as 1 -defined Function;

      set f = ( [:1, X:] * [:X, {1}:]), g = ( [: {1}, X:] * [:X, { 0 }:]), ff = (1 --> 1), gg = ( {1} --> 0 );

      

       B0: ff = f & gg = g by FOMODEL0: 73;

      ((I +* ff) +* gg) = sw by CARD_1: 49;

      hence thesis by B0;

    end;

    definition

      let v be Function;

      :: HILBERT4:def6

      func v tohilbperm -> set equals the set of all [n, ((v . n) tohilb )] where n be Element of NAT ;

      coherence ;

    end

    definition

      let v be Function;

      :: HILBERT4:def7

      func v tohilbval -> set equals the set of all [n, ( dom ((v . n) tohilb ))] where n be Element of NAT ;

      coherence ;

    end

    defpred P[ set] means not contradiction;

    

     Lm15: for v be Function holds (v tohilbval ) is Function & (v tohilbperm ) is Function & (( proj1 (v tohilbval )) = NAT & ( proj1 (v tohilbperm )) = NAT )

    proof

      let v be Function;

      set f = (v tohilbval ), g = (v tohilbperm );

      deffunc Ff( set) = ( dom ((v . $1) tohilb ));

      deffunc Fg( set) = ((v . $1) tohilb );

      set ff = { [n, Ff(n)] where n be Element of NAT : P[n] }, gg = { [n, Fg(n)] where n be Element of NAT : P[n] }, N = { n where n be Element of NAT : P[n] };

      

       B10: ff is Function from FOMODEL0:sch 3;

      hence f is Function;

      reconsider f as Function by B10;

      

       B11: gg is Function from FOMODEL0:sch 3;

      hence g is Function;

      reconsider g as Function by B11;

      

       B0: f = ff;

      

       BB2: ( dom f) = N from ALTCAT_2:sch 2( B0);

      

       B1: g = gg;

      ( dom g) = N from ALTCAT_2:sch 2( B1);

      hence thesis by BB2, FOMODEL0: 74;

    end;

    registration

      let v be Function;

      cluster (v tohilbval ) -> Function-like Relation-like;

      coherence by Lm15;

      cluster (v tohilbperm ) -> Function-like Relation-like;

      coherence by Lm15;

      cluster (v tohilbval ) -> NAT -defined;

      coherence by Lm15;

      cluster (v tohilbval ) -> total;

      coherence

      proof

        ( dom (v tohilbval )) = NAT by Lm15;

        hence thesis by PARTFUN1:def 2;

      end;

      cluster (v tohilbperm ) -> NAT -defined;

      coherence by Lm15;

      cluster (v tohilbperm ) -> total;

      coherence

      proof

        ( dom (v tohilbperm )) = NAT by Lm15;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    

     Lm34: x is Nat implies (((g tohilbperm ) . x) = ((g . x) tohilb ) & ((g tohilbval ) . x) = ( dom ((g . x) tohilb )))

    proof

      set fv = (g tohilbval ), fp = (g tohilbperm );

      assume x is Nat;

      then

      reconsider n = x as Element of NAT by ORDINAL1:def 12;

      deffunc F( set) = ((g . $1) tohilb );

      

       B0: P[n];

      

       B1: fp = { [o, F(o)] where o be Element of NAT : P[o] };

      (fp . n) = F(n) from ALTCAT_2:sch 3( B1, B0);

      hence (fp . x) = ((g . x) tohilb );

      deffunc G( set) = ( dom F($1));

      

       B2: fv = { [o, G(o)] where o be Element of NAT : P[o] };

      (fv . n) = G(n) from ALTCAT_2:sch 3( B2, B0);

      hence thesis;

    end;

    registration

      let v be Function;

      cluster (v tohilbval ) -> non-empty;

      coherence

      proof

        set f = (v tohilbval ), D = ( dom f), C = ( rng f);

        assume not f is non-empty;

        then

        consider x be object such that

         B0: x in D & {} = (f . x) by FUNCT_1:def 3;

        reconsider n = x as Element of NAT by B0;

        (f . n) = ( dom ((v . n) tohilb )) by Lm34;

        hence contradiction by CARD_1: 49, B0;

      end;

    end

    

     Lm37: (x tohilb ) is symmetric & ( dom (x tohilb )) = ( rng (x tohilb ))

    proof

      set g = (x tohilb );

      per cases ;

        suppose

         C00: x <> {} ;

        then

         C0: g = I by Lm18;

        thus g is symmetric by C00;

        thus thesis by C0;

      end;

        suppose

         C1: x = {} ;

        thus g is symmetric by C1, Lm17;

        ( dom sw) = { 0 , 1} & ( rng sw) = { 0 , 1} by FUNCT_4: 62, FUNCT_4: 64;

        hence thesis by C1, Lm17;

      end;

    end;

    registration

      let x;

      cluster (x tohilb ) -> symmetric;

      coherence by Lm37;

    end

    definition

      let v be Function;

      :: original: tohilbperm

      redefine

      func v tohilbperm -> Permutation of (v tohilbval ) ;

      coherence

      proof

        set fP = (v tohilbperm ), fV = (v tohilbval );

         B0:

        now

          (( dom fP) \+\ NAT ) = {} ;

          hence ( dom fP) = NAT by FOMODEL0: 29;

        end;

        now

          let n be Element of NAT ;

          

           D0: (fP . n) = ((v . n) tohilb ) & (fV . n) = ( dom ((v . n) tohilb )) by Lm34;

          then

          reconsider y = (fP . n) as symmetric Function;

          ( dom y) = (fV . n) & ( rng y) = ( dom y) by D0, Lm37;

          then y is onto Function of (fV . n), (fV . n) by FOMODEL0: 75;

          hence (fP . n) is Permutation of (fV . n);

        end;

        hence thesis by HILBERT3:def 4, B0;

      end;

    end

    definition

      mode SetValuation0 is ManySortedSet of NAT ;

    end

    reserve v for SetValuation0;

    registration

      let p, v;

      cluster ( Perm ((v tohilbperm ),p)) -> involutive;

      coherence

      proof

        set P = (v tohilbperm ), V = (v tohilbval ), fP = ( Perm P);

        defpred P[ set] means for f be Function st f = (fP . $1) holds f is involutive;

        

         A0: P[ VERUM ] by HILBERT3:def 5;

        

         A1: for n be Element of NAT holds P[( prop n)]

        proof

          let n be Element of NAT ;

          let f be Function;

          assume f = (fP . ( prop n));

          

          then f = (P . n) by HILBERT3:def 5

          .= ((v . n) tohilb ) by Lm34;

          hence thesis;

        end;

        

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

        proof

          let r, s;

          set a = (r '&' s), i = (r => s), f = ( Perm (P,r)), h = ( Perm (P,s)), F = ( SetVal (V,r)), H = ( SetVal (V,s));

          assume

           B1: P[r] & P[s];

          reconsider f as involutive Permutation of F by B1;

          reconsider h as involutive Permutation of H by B1;

          thus P[a]

          proof

            let g;

            assume g = (fP . a);

            

            then g = ( Perm (P,a))

            .= [:f, h:] by HILBERT3: 35;

            hence thesis;

          end;

          let F be Function;

          assume F = (fP . i);

          

          then F = ( Perm (P,i))

          .= (f => h) by HILBERT3: 36;

          hence thesis;

        end;

        for p holds P[p] from HILBERT2:sch 2( A0, A1, A2);

        hence thesis;

      end;

    end

    begin

    definition

      let V be SetValuation0;

      :: HILBERT4:def8

      func SetVal0 V -> ManySortedSet of HP-WFF means

      : Def2: (it . VERUM ) = 1 & (for n holds (it . ( prop n)) = (V . n)) & for p, q holds (it . (p '&' q)) = [:(it . p), (it . q):] & (it . (p => q)) = ( Funcs ((it . p),(it . q)));

      existence

      proof

        deffunc F( Element of NAT ) = (V . $1);

        consider M be ManySortedSet of HP-WFF such that

         A1: ((M . VERUM ) = 1 & for n holds (M . ( prop n)) = F(n)) & for p, q holds (M . (p '&' q)) = [:(M . p), (M . q):] & (M . (p => q)) = ( Funcs ((M . p),(M . q))) from HILBERT2:sch 4;

        take M;

        thus thesis by A1;

      end;

      uniqueness

      proof

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

         A2: (M1 . VERUM ) = 1 and

         A3: for n holds (M1 . ( prop n)) = (V . n) and

         A4: for p, q holds (M1 . (p '&' q)) = [:(M1 . p), (M1 . q):] & (M1 . (p => q)) = ( Funcs ((M1 . p),(M1 . q))) and

         A5: (M2 . VERUM ) = 1 and

         A6: for n holds (M2 . ( prop n)) = (V . n) and

         A7: for p, q holds (M2 . (p '&' q)) = [:(M2 . p), (M2 . q):] & (M2 . (p => q)) = ( Funcs ((M2 . p),(M2 . q)));

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

        

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

        proof

          let r, s such that

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

          

          thus (M1 . (r '&' s)) = [:(M2 . r), (M2 . s):] by A4, A9

          .= (M2 . (r '&' s)) by A7;

          

          thus (M1 . (r => s)) = ( Funcs ((M2 . r),(M2 . s))) by A4, A9

          .= (M2 . (r => s)) by A7;

        end;

        

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

        proof

          let n;

          

          thus (M1 . ( prop n)) = (V . n) by A3

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

        end;

        

         A11: P[ VERUM ] by A2, A5;

        for r holds P[r] from HILBERT2:sch 2( A11, A10, A8);

        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 v, p;

      :: HILBERT4:def9

      func SetVal0 (v,p) -> set equals (( SetVal0 v) . p);

      correctness ;

    end

    

     Lm100: ( fixpoints ( Perm ((v tohilbperm ),p))) <> {} iff ( SetVal0 (v,p)) <> {}

    proof

      set V = (v tohilbval ), P = (v tohilbperm ), fP = ( Perm P), fv = ( SetVal0 v), fV = ( SetVal V), I = ( id 1);

      defpred Z[ set] means (fv . $1) = {} iff ( fixpoints (fP . $1)) = {} ;

      

       A1: Z[ VERUM ]

      proof

        ( fixpoints (fP . VERUM )) = ( fixpoints I) by HILBERT3:def 5

        .= 1;

        hence thesis by Def2;

      end;

      

       A2: for n be Element of NAT holds Z[( prop n)]

      proof

        let n be Element of NAT ;

        set l = ( prop n), x = (fv . n), X = (fV . n);

        

         B0: (fP . l) = (P . n) & (fv . l) = (v . n) by Def2, HILBERT3:def 5;

        thus (fv . l) = {} implies ( fixpoints (fP . l)) = {}

        proof

          assume (fv . l) = {} ;

          then (P . n) = sw by B0, Lm34, Lm17;

          hence thesis by B0;

        end;

        assume

         B1: ( fixpoints (fP . l)) = {} ;

        assume (fv . l) <> {} ;

        then (v . n) <> {} & (P . n) = ((v . n) tohilb ) by Def2, Lm34;

        then (P . n) = I by Lm18;

        hence contradiction by CARD_1: 49, B1, B0;

      end;

      

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

      proof

        let r, s;

        set a = (r '&' s), i = (r => s);

        set F = ( SetVal (V,r)), H = ( SetVal (V,s));

        set f = ( Perm (P,r)), h = ( Perm (P,s));

        reconsider h as non empty involutive Permutation of H;

        reconsider ff = (f " ) as non empty involutive Permutation of F;

        set S = ( SomePoints ff), O = ( OtherPoints ff);

        reconsider S, O as Subset of ( field ff);

        set f1 = (ff | S), f2 = (ff | O);

        assume

         B0: Z[r] & Z[s];

        reconsider Sr = ( SetVal0 (v,r)), Ss = ( SetVal0 (v,s)) as set;

        ( SetVal0 (v,a)) = [:Sr, Ss:] by Def2;

        then ( SetVal0 (v,a)) = {} iff [:( fixpoints ( Perm (P,r))), ( fixpoints ( Perm (P,s))):] = {} by B0;

        then ( SetVal0 (v,a)) = {} iff ( fixpoints [:( Perm (P,r)), ( Perm (P,s)):]) = {} by FOMODEL0: 76;

        then ( SetVal0 (v,a)) = {} iff ( fixpoints ( Perm (P,a))) = {} by HILBERT3: 35;

        hence (fv . a) = {} iff ( fixpoints (fP . a)) = {} ;

        thus (fv . i) = {} implies ( fixpoints (fP . i)) = {}

        proof

          assume (fv . i) = {} ;

          then {} = ( Funcs ((fv . r),(fv . s))) by Def2;

          then f is with_fixpoint & h is without_fixpoints by B0;

          then ( Perm (P,i)) is without_fixpoints by Lm3;

          hence thesis;

        end;

        assume

         B2: ( fixpoints (fP . i)) = {} ;

        assume

         B3: (fv . i) <> {} ;

        per cases ;

          suppose (fv . s) <> {} ;

          then h is with_fixpoint by B0;

          then ( Perm (P,i)) is with_fixpoint by Lm2;

          hence contradiction by B2;

        end;

          suppose

           CCCC20: (fv . s) = {} ;

          then ( Funcs ((fv . r),(fv . s))) <> {} & (fv . s) = {} by B3, Def2;

          then

           CC20: (fv . s) = {} & (fv . r) = {} & (( fixpoints ff) \+\ ( fixpoints f)) = {} ;

          

           C00: ( dom ff) = F & ( dom h) = H & ( rng h) c= H & ( rng ff) c= F by PARTFUN1:def 2;

          

           C01: ( field ff) = (F null ( rng ff)) & ( field h) = (H null ( rng h)) by PARTFUN1:def 2;

          

           C0: ( dom ff) = F & ( dom h) = H & ( rng h) c= H & ( rng ff) c= F & ( field ff) = F & ( field h) = H & ( dom f1) = S & ( dom f2) = O & (ff .: O) = S & (ff .: S) = O & ( rng f1) = (ff .: S) & ( rng f2) = (ff .: O) by C00, C01, Lm30;

          then

           C2: (( rng f1) /\ ( rng f2)) = {} & ( rng f1) = ( dom f2) & ( rng f2) = ( dom f1);

          reconsider S, O as Subset of ( dom ff) by PARTFUN1:def 2, C01;

          (( rng h) \ ( dom h)) = {} & (( field h) \ ( fixpoints h)) <> {} by CCCC20, B0;

          then

          reconsider SH = ( SomePoints h), OH = ( OtherPoints h) as non empty Subset of ( dom h) by PARTFUN1:def 2, C01, Lm26;

          set b1 = the Element of SH, b2 = (h . b1);

          b2 in (h .: SH) & (h .: SH) c= OH by Lm23, FUNCT_1: 108;

          then b2 in OH & not b2 in (OH /\ SH);

          then

           C21: b1 <> b2 by XBOOLE_0:def 4;

          reconsider b1 as Element of ( dom h);

          set b2 = (h . b1), ha = ((b1,b2) --> (b2,b1)), hb = (h \ ha), g1 = [:( rng f1), {b2}:], g2 = [:( rng f2), {b1}:], g = (g1 \/ g2), h1 = (b1 .--> b2), h2 = (b2 .--> b1);

          (h . b2) = b1 & b2 in ( dom h) by C00;

          then

          reconsider h1, h2 as Function-like Relation-like Subset of h by FUNCT_4: 85;

          (h1 \/ h2) c= h & (h1 +*1 h2) c= (h1 \/ h2);

          then

          reconsider hha = ha as Function-like Relation-like Subset of h by XBOOLE_1: 1;

          h = ((h /\ ha) \/ hb);

          then

           C14: (((f1 \/ f2) * g) * h) = ((((f1 \/ f2) * g) * (hha null h)) \/ (((f1 \/ f2) * g) * hb)) by RELAT_1: 32;

          

           CC13: ( dom ha) = {b1, b2} & ( dom (h \ hha)) = (( dom h) \ ( dom ha)) by FOMODEL0: 78, FUNCT_4: 62;

          ( rng g1) c= {b2} & ( {b2} \ {b1, b2}) = {} ;

          then ( rng g1) c= {b2} & {b2} c= {b1, b2} by FOMODEL0: 29;

          then

          reconsider rg1 = ( rng g1) as Subset of {b1, b2} by XBOOLE_1: 1;

          ( rng g2) c= {b1} & ( {b1} \ {b1, b2}) = {} ;

          then ( rng g2) c= {b1} & {b1} c= {b1, b2} by FOMODEL0: 29;

          then

          reconsider rg2 = ( rng g2) as Subset of {b1, b2} by XBOOLE_1: 1;

          ((rg1 \/ rg2) \+\ ( rng g)) = {} & ((rg1 \/ rg2) \ {b1, b2}) = {} ;

          then

          reconsider rg = ( rng g) as Subset of {b1, b2} by FOMODEL0: 29;

          ( rng ((f1 \/ f2) >*> g)) c= rg by RELAT_1: 26;

          then

          reconsider R = ( rng ((f1 \/ f2) >*> g)) as Subset of {b1, b2} by XBOOLE_1: 1;

          (( dom hb) /\ R) = {} by CC13;

          then (((f1 \/ f2) >*> g) >*> hb) = {} by XBOOLE_0:def 7, RELAT_1: 44;

          then

           C15: g c= (((f1 \/ f2) >*> g) >*> h) by C14, C2, FOMODEL0: 77, C21;

          

           CC3: (S /\ O) = {} ;

          

           CC8: (( dom g1) \ ( dom g2)) = ( dom g1) & (( dom f1) \ ( dom f2)) = ( dom f1) by C0, CC3, XBOOLE_0:def 7, XBOOLE_1: 83;

          reconsider rff = ( rng ff) as Subset of F;

          

           C10: F = ((( field ff) \ S) \/ (( field ff) /\ S)) by C01

          .= ((( field ff) \ S) \/ (( dom ff) /\ S)) by C01, PARTFUN1:def 2

          .= ((O null ( dom ff)) \/ S) by CC20, B0;

          ((f1 \/ f2) \ ff) = {} & ((( dom f1) \/ ( dom f2)) \+\ ( dom (f1 \/ f2))) = {} ;

          then (f1 \/ f2) c= ff & ( dom (f1 \/ f2)) = F by C10, FOMODEL0: 29;

          then (f1 \/ f2) = ff by C00, FOMODEL0: 68;

          then

           C12: (g1 +* g2) c= ((h * (g1 +* g2)) * ff) by CC8, C15, RELAT_1: 36;

          ((( dom g1) \/ ( dom g2)) \+\ ( dom (g1 \/ g2))) = {} ;

          then

           C11: ( dom (g1 +* g2)) = F by C0, C10, CC8, FOMODEL0: 29;

          ( dom ((h * (g1 +* g2)) * ff)) c= ( dom (g1 +* g2)) by C11;

          then

           C17: (g1 +* g2) = ((h * (g1 +* g2)) * ff) by C12, FOMODEL0: 68;

          reconsider bb1 = b1, bb2 = b2 as Element of H;

          reconsider B = {bb1, bb2} as non empty Subset of H;

          rg c= {b1, b2};

          then

          reconsider gg = (g1 +* g2) as Element of ( Funcs (F,B)) by CC8, C11, FUNCT_2:def 2;

          gg is H -valued;

          then ( {gg} \ ( Funcs (F,H))) = {} ;

          then

          reconsider gg as Element of ( Funcs (F,H)) by FOMODEL0: 29;

          (( Perm (P,i)) . gg) = gg & gg <> {} by C17, HILBERT3: 37;

          then (( Perm (P,i)) . gg) = gg & gg in ( dom ( Perm (P,i))) by FUNCT_1:def 2;

          then gg is_a_fixpoint_of ( Perm (P,i)) by ABIAN:def 3;

          hence contradiction by B2, FOMODEL0: 69;

        end;

      end;

      for r holds Z[r] from HILBERT2:sch 2( A1, A2, A3);

      hence thesis;

    end;

    definition

      let p;

      :: HILBERT4:def10

      attr p is classical means

      : DefClassical: ( SetVal0 (v,p)) <> {} ;

    end

    registration

      cluster pseudo-canonical -> classical for Element of HP-WFF ;

      coherence

      proof

        let p;

        assume

         AA: p is pseudo-canonical;

        defpred IT[ Function] means ex x be set st x is_a_fixpoint_of $1;

        assume not p is classical;

        then

        consider v such that

         B0: ( SetVal0 (v,p)) = {} ;

        set P = (v tohilbperm ), V = (v tohilbval );

        ( fixpoints ( Perm (P,p))) = {} by Lm100, B0;

        then not IT[( Perm (P,p))] by FOMODEL0: 69;

        hence thesis by AA, HILBERT3:def 8;

      end;

    end

    registration

      let v;

      let p be classical Element of HP-WFF ;

      cluster ( SetVal0 (v,p)) -> non empty;

      coherence by DefClassical;

    end