hilbert3.miz



    begin

    registration

      let m,n be non zero Nat;

      cluster (( 0 ,n) --> (m, 0 )) -> one-to-one;

      coherence

      proof

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

        let x1,x2 be object;

        assume that

         A1: x1 in ( dom f) and

         A2: x2 in ( dom f);

        

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

        then

         A4: x2 = 0 or x2 = n by A2, TARSKI:def 2;

        

         A5: (f . 0 ) = m by FUNCT_4: 63;

        x1 = 0 or x1 = n by A3, A1, TARSKI:def 2;

        hence thesis by A4, A5, FUNCT_4: 63;

      end;

      cluster ((n, 0 ) --> ( 0 ,m)) -> one-to-one;

      coherence

      proof

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

        let x1,x2 be object;

        assume that

         A6: x1 in ( dom f) and

         A7: x2 in ( dom f);

        

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

        then

         A9: x2 = 0 or x2 = n by A7, TARSKI:def 2;

        

         A10: (f . 0 ) = m by FUNCT_4: 63;

        x1 = 0 or x1 = n by A8, A6, TARSKI:def 2;

        hence thesis by A9, A10, FUNCT_4: 63;

      end;

    end

    theorem :: HILBERT3:1

    for i be Integer holds i is even iff (i - 1) is odd;

    theorem :: HILBERT3:2

    for i be Integer holds i is odd iff (i - 1) is even;

    theorem :: HILBERT3:3

    

     Th3: for X be trivial set, x be set st x in X holds for f be Function of X, X holds x is_a_fixpoint_of f

    proof

      let X be trivial set, x be set;

      assume

       A1: x in X;

      then

      consider y be object such that

       A2: X = {y} by ZFMISC_1: 131;

      let f be Function of X, X;

      thus x in ( dom f) by A1, FUNCT_2: 52;

      then

       A3: (f . x) in ( rng f) by FUNCT_1:def 3;

      

       A4: ( rng f) c= X by RELAT_1:def 19;

      

      thus x = y by A1, A2, TARSKI:def 1

      .= (f . x) by A2, A3, A4, TARSKI:def 1;

    end;

    ::$Canceled

    theorem :: HILBERT3:5

    

     Th4: for A,B,x be set, f be Function st x in A & f in ( Funcs (A,B)) holds (f . x) in B

    proof

      let A,B,x be set, f be Function such that

       A1: x in A;

      assume

       A2: f in ( Funcs (A,B));

      then

       A3: f is Function of A, B by FUNCT_2: 66;

      B = {} implies A = {} by A2;

      hence thesis by A1, A3, FUNCT_2: 5;

    end;

    theorem :: HILBERT3:6

    

     Th5: for A,B,C be set st C = {} implies B = {} or A = {} holds for f be Function of A, ( Funcs (B,C)) holds ( doms f) = (A --> B)

    proof

      let A,B,C be set;

      assume C = {} implies B = {} or A = {} ;

      then

       A1: ( Funcs (B,C)) = {} implies A = {} by FUNCT_2: 8;

      let f be Function of A, ( Funcs (B,C));

      reconsider g = f as ManySortedFunction of A by A1;

      now

        let i be object;

        assume

         A2: i in A;

        then

         A3: (g . i) in ( Funcs (B,C)) by A1, FUNCT_2: 5;

        

        thus (( doms g) . i) = ( dom (g . i)) by A2, MSSUBFAM: 14

        .= B by A3, FUNCT_2: 92

        .= ((A --> B) . i) by A2, FUNCOP_1: 7;

      end;

      hence thesis by PBOOLE: 3;

    end;

    reserve n for Element of NAT ,

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

    theorem :: HILBERT3:7

    for x be set holds ( {} . x) = {} ;

    theorem :: HILBERT3:8

    

     Th7: for X be set, A be Subset of X holds ((( 0 ,1) --> (1, 0 )) * ( chi (A,X))) = ( chi ((A ` ),X))

    proof

      let X be set, A be Subset of X;

      set f = ((( 0 ,1) --> (1, 0 )) * ( chi (A,X)));

      

       A1: ( dom ( chi (A,X))) = X by FUNCT_3:def 3;

      

       A2: for x be object st x in X holds (x in (A ` ) implies (f . x) = 1) & ( not x in (A ` ) implies (f . x) = 0 )

      proof

        let x be object such that

         A3: x in X;

        thus x in (A ` ) implies (f . x) = 1

        proof

          assume x in (A ` );

          then not x in A by XBOOLE_0:def 5;

          then (( chi (A,X)) . x) = 0 by A3, FUNCT_3:def 3;

          then (f . x) = ((( 0 ,1) --> (1, 0 )) . 0 ) by A1, A3, FUNCT_1: 13;

          hence thesis by FUNCT_4: 63;

        end;

        assume not x in (A ` );

        then x in A by A3, XBOOLE_0:def 5;

        then (( chi (A,X)) . x) = 1 by FUNCT_3:def 3;

        then (f . x) = ((( 0 ,1) --> (1, 0 )) . 1) by A1, A3, FUNCT_1: 13;

        hence thesis by FUNCT_4: 63;

      end;

      ( dom (( 0 ,1) --> (1, 0 ))) = { 0 , 1} by FUNCT_4: 62;

      then ( rng ( chi (A,X))) c= ( dom (( 0 ,1) --> (1, 0 ))) by FUNCT_3: 39;

      hence thesis by A2, FUNCT_3:def 3, A1, RELAT_1: 27;

    end;

    theorem :: HILBERT3:9

    

     Th8: for X be set, A be Subset of X holds ((( 0 ,1) --> (1, 0 )) * ( chi ((A ` ),X))) = ( chi (A,X))

    proof

      let X be set, A be Subset of X;

      ((A ` ) ` ) = A;

      hence thesis by Th7;

    end;

    theorem :: HILBERT3:10

    

     Th9: for a,b,x,y,x9,y9 be set st a <> b & ((a,b) --> (x,y)) = ((a,b) --> (x9,y9)) holds x = x9 & y = y9

    proof

      let a,b,x,y,x9,y9 be set such that

       A1: a <> b and

       A2: ((a,b) --> (x,y)) = ((a,b) --> (x9,y9));

      

      thus x = (((a,b) --> (x,y)) . a) by A1, FUNCT_4: 63

      .= x9 by A1, A2, FUNCT_4: 63;

      

      thus y = (((a,b) --> (x,y)) . b) by FUNCT_4: 63

      .= y9 by A2, FUNCT_4: 63;

    end;

    theorem :: HILBERT3:11

    

     Th10: for a,b,x,y,X,Y be set st a <> b & x in X & y in Y holds ((a,b) --> (x,y)) in ( product ((a,b) --> (X,Y)))

    proof

      let a,b,x,y,X,Y be set such that

       A1: a <> b and

       A2: x in X & y in Y;

       {x} c= X & {y} c= Y by A2, ZFMISC_1: 31;

      then ( product ((a,b) --> ( {x}, {y}))) c= ( product ((a,b) --> (X,Y))) by TOPREAL6: 21;

      then {((a,b) --> (x,y))} c= ( product ((a,b) --> (X,Y))) by A1, CARD_3: 47;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: HILBERT3:12

    

     Th11: for D be non empty set holds for f be Function of 2, D holds ex d1,d2 be Element of D st f = (( 0 ,1) --> (d1,d2))

    proof

      let D be non empty set;

      let f be Function of 2, D;

       0 in 2 & 1 in 2 by CARD_1: 50, TARSKI:def 2;

      then

      reconsider d1 = (f . 0 ), d2 = (f . 1) as Element of D by FUNCT_2: 5;

      take d1, d2;

      ( dom f) = { 0 , 1} by CARD_1: 50, FUNCT_2:def 1;

      hence thesis by FUNCT_4: 66;

    end;

    theorem :: HILBERT3:13

    

     Th12: for a,b,c,d be set st a <> b holds (((a,b) --> (c,d)) * ((a,b) --> (b,a))) = ((a,b) --> (d,c))

    proof

      let a,b,c,d be set such that

       A1: a <> b;

      set f = (((a,b) --> (c,d)) * ((a,b) --> (b,a)));

      

       A2: ( dom ((a,b) --> (b,a))) = {a, b} by FUNCT_4: 62;

      b in {a, b} by TARSKI:def 2;

      

      then

       A3: (f . b) = (((a,b) --> (c,d)) . (((a,b) --> (b,a)) . b)) by A2, FUNCT_1: 13

      .= (((a,b) --> (c,d)) . a) by FUNCT_4: 63

      .= c by A1, FUNCT_4: 63;

      a in {a, b} by TARSKI:def 2;

      

      then

       A4: (f . a) = (((a,b) --> (c,d)) . (((a,b) --> (b,a)) . a)) by A2, FUNCT_1: 13

      .= (((a,b) --> (c,d)) . b) by A1, FUNCT_4: 63

      .= d by FUNCT_4: 63;

      ( rng ((a,b) --> (b,a))) = {a, b} by A1, FUNCT_4: 64

      .= ( dom ((a,b) --> (c,d))) by FUNCT_4: 62;

      hence thesis by A4, A3, FUNCT_4: 66, A2, RELAT_1: 27;

    end;

    theorem :: HILBERT3:14

    

     Th13: for a,b,c,d be set, f be Function st a <> b & c in ( dom f) & d in ( dom f) holds (f * ((a,b) --> (c,d))) = ((a,b) --> ((f . c),(f . d)))

    proof

      let a,b,c,d be set, f be Function such that

       A1: a <> b and

       A2: c in ( dom f) & d in ( dom f);

      

       A3: ( dom ((a,b) --> (c,d))) = {a, b} by FUNCT_4: 62;

      then a in ( dom ((a,b) --> (c,d))) by TARSKI:def 2;

      

      then

       A4: ((f * ((a,b) --> (c,d))) . a) = (f . (((a,b) --> (c,d)) . a)) by FUNCT_1: 13

      .= (f . c) by A1, FUNCT_4: 63;

      b in ( dom ((a,b) --> (c,d))) by A3, TARSKI:def 2;

      

      then

       A5: ((f * ((a,b) --> (c,d))) . b) = (f . (((a,b) --> (c,d)) . b)) by FUNCT_1: 13

      .= (f . d) by FUNCT_4: 63;

      

       A6: ( rng ((a,b) --> (c,d))) c= {c, d} by FUNCT_4: 62;

       {c, d} c= ( dom f) by A2, ZFMISC_1: 32;

      then ( dom (f * ((a,b) --> (c,d)))) = {a, b} by A3, A6, RELAT_1: 27, XBOOLE_1: 1;

      hence thesis by A4, A5, FUNCT_4: 66;

    end;

    theorem :: HILBERT3:15

    

     Th14: (( 0 ,1) --> (1, 0 )) is Permutation of 2

    proof

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

      

       A1: ( rng f) = 2 by CARD_1: 50, FUNCT_4: 64;

      ( dom f) = 2 by CARD_1: 50, FUNCT_4: 62;

      then f is Function of 2, 2 by A1, FUNCT_2:def 1, RELSET_1: 4;

      hence thesis by A1, FUNCT_2: 57;

    end;

    begin

    registration

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

      cluster [:f, g:] -> one-to-one;

      coherence

      proof

        let x,y be object such that

         A1: x in ( dom [:f, g:]) and

         A2: y in ( dom [:f, g:]) and

         A3: ( [:f, g:] . x) = ( [:f, g:] . y);

        

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

        then

        consider x1,x2 be object such that

         A5: x1 in ( dom f) and

         A6: x2 in ( dom g) and

         A7: x = [x1, x2] by A1, ZFMISC_1:def 2;

        

         A8: ( [:f, g:] . (x1,x2)) = [(f . x1), (g . x2)] by A5, A6, FUNCT_3:def 8;

        consider y1,y2 be object such that

         A9: y1 in ( dom f) and

         A10: y2 in ( dom g) and

         A11: y = [y1, y2] by A2, A4, ZFMISC_1:def 2;

        

         A12: ( [:f, g:] . (y1,y2)) = [(f . y1), (g . y2)] by A9, A10, FUNCT_3:def 8;

        then (f . x1) = (f . y1) by A3, A7, A11, A8, XTUPLE_0: 1;

        then

         A13: x1 = y1 by A5, A9, FUNCT_1:def 4;

        (g . x2) = (g . y2) by A3, A7, A11, A8, A12, XTUPLE_0: 1;

        hence thesis by A6, A7, A10, A11, A13, FUNCT_1:def 4;

      end;

    end

    theorem :: HILBERT3:16

    

     Th15: for A,B be non empty set, C,D be set, f be Function of C, A, g be Function of D, B holds (( pr1 (A,B)) * [:f, g:]) = (f * ( pr1 (C,D)))

    proof

      let A,B be non empty set, C,D be set;

      let f be Function of C, A, g be Function of D, B;

      C = {} implies A = {} or [:C, D:] = {} ;

      then

      reconsider F = (f * ( pr1 (C,D))) as Function of [:C, D:], A;

      D = {} implies A = {} or [:C, D:] = {} ;

      then

      reconsider G = (g * ( pr2 (C,D))) as Function of [:C, D:], B;

      

      thus (( pr1 (A,B)) * [:f, g:]) = (( pr1 (A,B)) * <:F, G:>) by FUNCT_3: 77

      .= (f * ( pr1 (C,D))) by FUNCT_3: 62;

    end;

    theorem :: HILBERT3:17

    

     Th16: for A,B be non empty set, C,D be set, f be Function of C, A, g be Function of D, B holds (( pr2 (A,B)) * [:f, g:]) = (g * ( pr2 (C,D)))

    proof

      let A,B be non empty set, C,D be set;

      let f be Function of C, A, g be Function of D, B;

      C = {} implies A = {} or [:C, D:] = {} ;

      then

      reconsider F = (f * ( pr1 (C,D))) as Function of [:C, D:], A;

      D = {} implies A = {} or [:C, D:] = {} ;

      then

      reconsider G = (g * ( pr2 (C,D))) as Function of [:C, D:], B;

      

      thus (( pr2 (A,B)) * [:f, g:]) = (( pr2 (A,B)) * <:F, G:>) by FUNCT_3: 77

      .= (g * ( pr2 (C,D))) by FUNCT_3: 62;

    end;

    theorem :: HILBERT3:18

    for g be Function holds ( {} .. g) = {}

    proof

      let g be Function;

      ( dom ( {} .. g)) = (( dom {} ) /\ ( dom g)) by PRALG_1:def 19

      .= ( dom {} );

      hence thesis;

    end;

    theorem :: HILBERT3:19

    

     Th18: for f be Function-yielding Function, g,h be Function st ( dom f) = ( dom g) holds ((f .. g) * h) = ((f * h) .. (g * h))

    proof

      let f be Function-yielding Function, g,h be Function;

      assume

       AA: ( dom f) = ( dom g);

      

       A0: ( dom ((f * h) .. (g * h))) = (( dom (f * h)) /\ ( dom (g * h))) by PRALG_1:def 19;

      

       A1: for x be set st x in ( dom ((f * h) .. (g * h))) holds (((f .. g) * h) . x) = (((f * h) . x) . ((g * h) . x))

      proof

        let x be set;

        assume x in ( dom ((f * h) .. (g * h)));

        then x in (( dom (f * h)) /\ ( dom (g * h))) by PRALG_1:def 19;

        then

         a3: x in ( dom (f * h)) & x in ( dom (g * h)) by XBOOLE_0:def 4;

        then

         A3: x in ( dom h) by FUNCT_1: 11;

        (h . x) in ( dom f) & (h . x) in ( dom g) by a3, FUNCT_1: 11;

        then (h . x) in (( dom f) /\ ( dom g)) by XBOOLE_0:def 4;

        then

         a4: (h . x) in ( dom (f .. g)) by PRALG_1:def 19;

        

        thus (((f .. g) * h) . x) = ((f .. g) . (h . x)) by A3, FUNCT_1: 13

        .= ((f . (h . x)) . (g . (h . x))) by PRALG_1:def 19, a4

        .= (((f * h) . x) . (g . (h . x))) by A3, FUNCT_1: 13

        .= (((f * h) . x) . ((g * h) . x)) by A3, FUNCT_1: 13;

      end;

      

       a1: ( dom (f * h)) = ( dom (g * h)) by AA, RELAT_1: 163;

      ( dom (f .. g)) = (( dom f) /\ ( dom g)) by PRALG_1:def 19

      .= ( dom f) by AA;

      then ( dom ((f .. g) * h)) = ( dom (f * h)) by RELAT_1: 163;

      hence thesis by A1, A0, PRALG_1:def 19, a1;

    end;

    theorem :: HILBERT3:20

    for C be set, A be non empty set holds for f be Function of A, ( Funcs ( {} qua set,C)), g be Function of A, {} holds ( rng (f .. g)) = {}

    proof

      let C be set, A be non empty set;

      let f be Function of A, ( Funcs ( {} qua set,C)), g be Function of A, {} ;

      set a = the Element of A;

      ( dom (f .. g)) = (( dom f) /\ ( dom g)) by PRALG_1:def 19

      .= {} ;

      hence thesis by RELAT_1: 42;

    end;

    theorem :: HILBERT3:21

    

     Th20: for A,B,C be set st (B = {} implies A = {} ) & (C = {} implies B = {} ) holds for f be Function of A, ( Funcs (B,C)), g be Function of A, B holds ( rng (f .. g)) c= C

    proof

      let A,B,C be set such that

       A1: B = {} implies A = {} and

       a1: C = {} implies B = {} ;

      let f be Function of A, ( Funcs (B,C)), g be Function of A, B;

      let x be object;

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

      then

      consider y be object such that

       A2: y in ( dom (f .. g)) and

       A3: ((f .. g) . y) = x by FUNCT_1:def 3;

      

       S1: ( dom f) = ( dom g)

      proof

        per cases ;

          suppose B <> {} ;

          then

           C1: ( dom g) = A by FUNCT_2:def 1;

          ( Funcs (B,C)) <> {} by a1, FUNCT_2: 8;

          hence thesis by C1, FUNCT_2:def 1;

        end;

          suppose B = {} ;

          hence thesis by A1;

        end;

      end;

      

       A4: ( dom (f .. g)) = (( dom f) /\ ( dom g)) by PRALG_1:def 19

      .= ( dom f) by S1;

      then

       A5: ( Funcs (B,C)) <> {} by A2;

      then

       A6: ( dom f) = A by FUNCT_2:def 1;

      then

      reconsider fy = (f . y) as Function of B, C by A2, A4, A5, FUNCT_2: 5, FUNCT_2: 66;

      

       A7: C <> {} by A1, A2, A4;

      (g . y) in B by A1, A2, A4, A6, FUNCT_2: 5;

      then (fy . (g . y)) in C by A7, FUNCT_2: 5;

      hence thesis by A2, A3, PRALG_1:def 19;

    end;

    theorem :: HILBERT3:22

    

     Th21: for A,B,C be set st C = {} implies B = {} or A = {} holds for f be Function of A, ( Funcs (B,C)) holds ( dom ( Frege f)) = ( Funcs (A,B))

    proof

      let A,B,C be set such that

       A1: C = {} implies B = {} or A = {} ;

      let f be Function of A, ( Funcs (B,C));

      

      thus ( dom ( Frege f)) = ( product ( doms f)) by PARTFUN1:def 2

      .= ( product (A --> B)) by A1, Th5

      .= ( Funcs (A,B)) by CARD_3: 11;

    end;

    theorem :: HILBERT3:23

    

     Th22: for A,B,C be set st C = {} implies B = {} or A = {} holds for f be Function of A, ( Funcs (B,C)) holds ( rng ( Frege f)) c= ( Funcs (A,C))

    proof

      let A,B,C be set;

      assume C = {} implies B = {} or A = {} ;

      then

       A1: ( Funcs (B,C)) = {} implies A = {} by FUNCT_2: 8;

      let f be Function of A, ( Funcs (B,C));

      

       A2: ( dom ( rngs f)) = ( dom f) by FUNCT_6:def 3;

      then

       A3: ( dom ( rngs f)) = A by A1, FUNCT_2:def 1;

      

       A4: for x be object st x in ( dom ( rngs f)) holds (( rngs f) . x) c= ((A --> C) . x)

      proof

        let x be object such that

         A5: x in ( dom ( rngs f));

        

         A6: (( rngs f) . x) = ( rng (f . x)) by A2, A5, FUNCT_6:def 3;

        (f . x) in ( Funcs (B,C)) by A1, A3, A5, FUNCT_2: 5;

        then (( rngs f) . x) c= C by A6, FUNCT_2: 92;

        hence thesis by A3, A5, FUNCOP_1: 7;

      end;

      ( dom ( rngs f)) = ( dom (A --> C)) by A3;

      then ( product ( rngs f)) c= ( product (A --> C)) by A4, CARD_3: 27;

      then ( product ( rngs f)) c= ( Funcs (A,C)) by CARD_3: 11;

      hence thesis by FUNCT_6: 38;

    end;

    theorem :: HILBERT3:24

    

     Th23: for A,B,C be set st C = {} implies B = {} or A = {} holds for f be Function of A, ( Funcs (B,C)) holds ( Frege f) is Function of ( Funcs (A,B)), ( Funcs (A,C))

    proof

      let A,B,C be set;

      assume

       A1: C = {} implies B = {} or A = {} ;

      then

       A2: ( Funcs (A,C)) = {} implies ( Funcs (A,B)) = {} by FUNCT_2: 8;

      let f be Function of A, ( Funcs (B,C));

      ( dom ( Frege f)) = ( Funcs (A,B)) & ( rng ( Frege f)) c= ( Funcs (A,C)) by A1, Th21, Th22;

      hence thesis by A2, FUNCT_2:def 1, RELSET_1: 4;

    end;

    begin

    registration

      let A,B be set, P be Permutation of A, Q be Permutation of B;

      cluster [:P, Q:] -> bijective;

      coherence

      proof

         [:P, Q:] is bijective

        proof

          thus [:P, Q:] is one-to-one;

          ( rng P) = A & ( rng Q) = B by FUNCT_2:def 3;

          hence ( rng [:P, Q:]) = [:A, B:] by FUNCT_3: 67;

        end;

        hence thesis;

      end;

    end

    theorem :: HILBERT3:25

    for A,B be set, P be Permutation of A, Q be Permutation of B holds [:P, Q:] is bijective;

    definition

      let A,B be non empty set;

      let P be Permutation of A, Q be Function of B, B;

      :: HILBERT3:def1

      func P => Q -> Function of ( Funcs (A,B)), ( Funcs (A,B)) means

      : Def1: for f be Function of A, B holds (it . f) = ((Q * f) * (P " ));

      existence

      proof

        deffunc F1( Element of ( Funcs (A,B))) = ((Q * $1) * (P " ));

        

         A1: for f be Element of ( Funcs (A,B)) holds F1(f) in ( Funcs (A,B)) by FUNCT_2: 8;

        consider F be Function of ( Funcs (A,B)), ( Funcs (A,B)) such that

         A2: for f be Element of ( Funcs (A,B)) holds (F . f) = F1(f) from FUNCT_2:sch 8( A1);

        take F;

        let f be Function of A, B;

        f in ( Funcs (A,B)) by FUNCT_2: 8;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let F,G be Function of ( Funcs (A,B)), ( Funcs (A,B)) such that

         A3: for f be Function of A, B holds (F . f) = ((Q * f) * (P " )) and

         A4: for f be Function of A, B holds (G . f) = ((Q * f) * (P " ));

        now

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

          

          thus (F . f) = ((Q * f) * (P " )) by A3

          .= (G . f) by A4;

        end;

        hence F = G;

      end;

    end

    registration

      let A,B be non empty set;

      let P be Permutation of A, Q be Permutation of B;

      cluster (P => Q) -> bijective;

      coherence

      proof

        thus (P => Q) is one-to-one

        proof

          let x1,x2 be object;

          assume x1 in ( dom (P => Q)) & x2 in ( dom (P => Q));

          then

          reconsider f1 = x1, f2 = x2 as Element of ( Funcs (A,B)) by FUNCT_2:def 1;

          assume ((P => Q) . x1) = ((P => Q) . x2);

          

          then

           A1: ((Q * f1) * (P " )) = ((P => Q) . f2) by Def1

          .= ((Q * f2) * (P " )) by Def1;

          

           A2: (Q * f1) = ((Q * f1) * ( id A)) by FUNCT_2: 17

          .= ((Q * f1) * ((P " ) * P)) by FUNCT_2: 61

          .= (((Q * f2) * (P " )) * P) by A1, RELAT_1: 36

          .= ((Q * f2) * ((P " ) * P)) by RELAT_1: 36

          .= ((Q * f2) * ( id A)) by FUNCT_2: 61

          .= (Q * f2) by FUNCT_2: 17;

          f1 = (( id B) * f1) by FUNCT_2: 17

          .= (((Q " ) * Q) * f1) by FUNCT_2: 61

          .= ((Q " ) * (Q * f2)) by A2, RELAT_1: 36

          .= (((Q " ) * Q) * f2) by RELAT_1: 36

          .= (( id B) * f2) by FUNCT_2: 61

          .= f2 by FUNCT_2: 17;

          hence thesis;

        end;

        thus ( rng (P => Q)) c= ( Funcs (A,B)) by RELAT_1:def 19;

        let x be object;

        assume x in ( Funcs (A,B));

        then x is Element of ( Funcs (A,B));

        then

        reconsider f = x as Function of A, B;

        ( dom (P => Q)) = ( Funcs (A,B)) by FUNCT_2:def 1;

        then

         A3: (((Q " ) * f) * P) in ( dom (P => Q)) by FUNCT_2: 8;

        ((P => Q) . (((Q " ) * f) * P)) = ((Q * (((Q " ) * f) * P)) * (P " )) by Def1

        .= (((Q * ((Q " ) * f)) * P) * (P " )) by RELAT_1: 36

        .= ((((Q * (Q " )) * f) * P) * (P " )) by RELAT_1: 36

        .= (((( id B) * f) * P) * (P " )) by FUNCT_2: 61

        .= ((f * P) * (P " )) by FUNCT_2: 17

        .= (f * (P * (P " ))) by RELAT_1: 36

        .= (f * ( id A)) by FUNCT_2: 61

        .= f by FUNCT_2: 17;

        hence x in ( rng (P => Q)) by A3, FUNCT_1:def 3;

      end;

    end

    theorem :: HILBERT3:26

    

     Th25: for A,B be non empty set holds for P be Permutation of A, Q be Permutation of B holds for f be Function of A, B holds (((P => Q) " ) . f) = (((Q " ) * f) * P)

    proof

      let A,B be non empty set;

      let P be Permutation of A, Q be Permutation of B;

      let f be Function of A, B;

      reconsider h = f as Element of ( Funcs (A,B)) by FUNCT_2: 8;

      reconsider g = (((Q " ) * f) * P) as Function of A, B;

      f in ( Funcs (A,B)) by FUNCT_2: 8;

      

      then

       A1: ((((P => Q) " ) " ) . (((P => Q) " ) . f)) = f by FUNCT_2: 26

      .= (f * ( id A)) by FUNCT_2: 17

      .= (f * (P * (P " ))) by FUNCT_2: 61

      .= ((f * P) * (P " )) by RELAT_1: 36

      .= (((( id B) * f) * P) * (P " )) by FUNCT_2: 17

      .= ((((Q * (Q " )) * f) * P) * (P " )) by FUNCT_2: 61

      .= (((Q * ((Q " ) * f)) * P) * (P " )) by RELAT_1: 36

      .= ((Q * (((Q " ) * f) * P)) * (P " )) by RELAT_1: 36

      .= ((P => Q) . g) by Def1

      .= ((((P => Q) " ) " ) . (((Q " ) * f) * P)) by FUNCT_1: 43;

      (((P => Q) " ) . h) in ( Funcs (A,B)) & g in ( Funcs (A,B)) by FUNCT_2: 8;

      hence thesis by A1, FUNCT_2: 19;

    end;

    theorem :: HILBERT3:27

    

     Th26: for A,B be non empty set holds for P be Permutation of A, Q be Permutation of B holds ((P => Q) " ) = ((P " ) => (Q " ))

    proof

      let A,B be non empty set;

      let P be Permutation of A, Q be Permutation of B;

      now

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

        

        thus (((P => Q) " ) . f) = (((Q " ) * f) * P) by Th25

        .= (((Q " ) * f) * ((P " ) " )) by FUNCT_1: 43

        .= (((P " ) => (Q " )) . f) by Def1;

      end;

      hence thesis;

    end;

    theorem :: HILBERT3:28

    

     Th27: for A,B,C be non empty set, f be Function of A, ( Funcs (B,C)), g be Function of A, B, P be Permutation of B, Q be Permutation of C holds (((P => Q) * f) .. (P * g)) = (Q * (f .. g))

    proof

      let A,B,C be non empty set;

      let f be Function of A, ( Funcs (B,C)), g be Function of A, B, P be Permutation of B, Q be Permutation of C;

      

       A1: ( dom ((P => Q) * f)) = A by FUNCT_2:def 1;

      

       A2: ( dom Q) = C & ( rng (f .. g)) c= C by Th20, FUNCT_2:def 1;

      

       A3: ( dom f) = A by FUNCT_2:def 1;

      

       a4: ( dom g) = A by FUNCT_2:def 1;

      

       B2: ( dom (f .. g)) = (( dom f) /\ ( dom g)) by PRALG_1:def 19

      .= A by A3, a4;

      then

       A4: ( dom (Q * (f .. g))) = A by A2, RELAT_1: 27;

      set gg = (Q * (f .. g));

      ( dom (P * g)) = A by FUNCT_2:def 1;

      then

       S1: ( dom gg) = (( dom ((P => Q) * f)) /\ ( dom (P * g))) by A4, A1;

      for x be set st x in ( dom gg) holds (gg . x) = ((((P => Q) * f) . x) . ((P * g) . x))

      proof

        let x be set such that

         a5: x in ( dom (Q * (f .. g)));

        

         A5: x in ( dom ((P => Q) * f)) by a5, A4, A1;

        reconsider fx = (f . x) as Function of B, C by A1, A5, FUNCT_2: 5, FUNCT_2: 66;

        (g . x) in B by A1, A5, FUNCT_2: 5;

        then

         A6: (g . x) in ( dom fx) by FUNCT_2:def 1;

        ((P * g) . x) in B by A1, A5, FUNCT_2: 5;

        then

         A7: ((P * g) . x) in ( dom (P " )) by FUNCT_2:def 1;

        

         B1: x in ( dom (f .. g)) by B2, A5, A1;

        

        thus ((Q * (f .. g)) . x) = (Q . ((f .. g) . x)) by A4, A1, A5, FUNCT_1: 12

        .= (Q . (fx . (g . x))) by B1, PRALG_1:def 19

        .= ((Q * fx) . (g . x)) by A6, FUNCT_1: 13

        .= ((Q * fx) . ((( id B) * g) . x)) by FUNCT_2: 17

        .= ((Q * fx) . ((((P " ) * P) * g) . x)) by FUNCT_2: 61

        .= ((Q * fx) . (((P " ) * (P * g)) . x)) by RELAT_1: 36

        .= ((Q * fx) . ((P " ) . ((P * g) . x))) by A1, A5, FUNCT_2: 15

        .= (((Q * fx) * (P " )) . ((P * g) . x)) by A7, FUNCT_1: 13

        .= (((P => Q) . fx) . ((P * g) . x)) by Def1

        .= ((((P => Q) * f) . x) . ((P * g) . x)) by A1, A5, FUNCT_2: 15;

      end;

      hence thesis by S1, PRALG_1:def 19;

    end;

    begin

    definition

      mode SetValuation is non-empty ManySortedSet of NAT ;

    end

    reserve V for SetValuation;

    definition

      let V;

      :: HILBERT3:def2

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

        hence M1 = M2;

      end;

    end

    definition

      let V, p;

      :: HILBERT3:def3

      func SetVal (V,p) -> set equals (( SetVal V) . p);

      correctness ;

    end

    registration

      let V, p;

      cluster ( SetVal (V,p)) -> non empty;

      coherence

      proof

        defpred P[ Element of HP-WFF ] means (( SetVal V) . $1) is non empty;

        

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

        proof

          let n;

          (( SetVal V) . ( prop n)) = (V . n) by Def2;

          hence thesis;

        end;

        

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

        proof

          let r, s such that

           A3: (( SetVal V) . r) is non empty and

           A4: (( SetVal V) . s) is non empty;

          (( SetVal V) . (r '&' s)) = [:(( SetVal V) . r), (( SetVal V) . s):] by Def2;

          hence (( SetVal V) . (r '&' s)) is non empty by A3, A4;

          (( SetVal V) . (r => s)) = ( Funcs ((( SetVal V) . r),(( SetVal V) . s))) by Def2;

          hence thesis by A4;

        end;

        

         A5: P[ VERUM ] by Def2;

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

        hence thesis;

      end;

    end

    theorem :: HILBERT3:29

    ( SetVal (V, VERUM )) = 1 by Def2;

    theorem :: HILBERT3:30

    ( SetVal (V,( prop n))) = (V . n) by Def2;

    theorem :: HILBERT3:31

    ( SetVal (V,(p '&' q))) = [:( SetVal (V,p)), ( SetVal (V,q)):] by Def2;

    theorem :: HILBERT3:32

    ( SetVal (V,(p => q))) = ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by Def2;

    registration

      let V, p, q;

      cluster ( SetVal (V,(p => q))) -> functional;

      coherence

      proof

        let x be object;

        assume x in ( SetVal (V,(p => q)));

        then x in ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by Def2;

        hence thesis;

      end;

    end

    registration

      let V, p, q, r;

      cluster -> Function-yielding for Element of ( SetVal (V,(p => (q => r))));

      coherence

      proof

        let e be Element of ( SetVal (V,(p => (q => r)))), x be object such that x in ( dom e);

        e in ( SetVal (V,(p => (q => r))));

        then e in ( Funcs (( SetVal (V,p)),( SetVal (V,(q => r))))) by Def2;

        then e is Function of ( SetVal (V,p)), ( SetVal (V,(q => r))) by FUNCT_2: 66;

        hence thesis;

      end;

    end

    registration

      let V, p, q, r;

      cluster Function-yielding for Function of ( SetVal (V,(p => q))), ( SetVal (V,(p => r)));

      existence

      proof

        set e = the Function of ( SetVal (V,(p => q))), ( SetVal (V,(p => r)));

        e is Function-yielding;

        hence thesis;

      end;

      cluster Function-yielding for Element of ( SetVal (V,(p => (q => r))));

      existence

      proof

        set e = the Element of ( SetVal (V,(p => (q => r))));

        e is Function-yielding;

        hence thesis;

      end;

    end

    begin

    definition

      let V;

      :: HILBERT3:def4

      mode Permutation of V -> Function means

      : Def4: ( dom it ) = NAT & for n holds (it . n) is Permutation of (V . n);

      existence

      proof

        take ( id V);

        thus ( dom ( id V)) = NAT by PARTFUN1:def 2;

        let n;

        (( id V) . n) = ( id (V . n)) by MSUALG_3:def 1;

        hence thesis;

      end;

    end

    reserve P for Permutation of V;

    definition

      let V, P;

      :: HILBERT3:def5

      func Perm P -> ManySortedFunction of ( SetVal V), ( SetVal V) means

      : Def5: (it . VERUM ) = ( id 1) & (for n holds (it . ( prop n)) = (P . n)) & for p, q holds ex p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q)) st p9 = (it . p) & q9 = (it . q) & (it . (p '&' q)) = [:p9, q9:] & (it . (p => q)) = (p9 => q9);

      existence

      proof

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

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

        defpred C[ Element of HP-WFF , Element of HP-WFF , set, set, set] means ($3 is Permutation of ( SetVal (V,$1)) & $4 is Permutation of ( SetVal (V,$2)) implies ex p9 be Permutation of ( SetVal (V,$1)), q9 be Permutation of ( SetVal (V,$2)) st p9 = $3 & q9 = $4 & $5 = [:p9, q9:]) & ( not $3 is Permutation of ( SetVal (V,$1)) or not $4 is Permutation of ( SetVal (V,$2)) 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 Permutation of ( SetVal (V,p)) and

             A3: b is Permutation of ( SetVal (V,q));

            reconsider q9 = b as Permutation of ( SetVal (V,q)) by A3;

            reconsider p9 = a as Permutation of ( SetVal (V,p)) by A2;

            take [:p9, q9:];

            thus thesis;

          end;

            suppose not a is Permutation of ( SetVal (V,p)) or not b is Permutation of ( SetVal (V,q));

            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 Permutation of ( SetVal (V,p)) and

             A6: b is Permutation of ( SetVal (V,q));

            reconsider q9 = b as Permutation of ( SetVal (V,q)) by A6;

            reconsider p9 = a as Permutation of ( SetVal (V,p)) by A5;

            take (p9 => q9);

            thus thesis;

          end;

            suppose not a is Permutation of ( SetVal (V,p)) or not b is Permutation of ( SetVal (V,q));

            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 ) = ( id 1) and

         A10: for n holds (M . ( prop n)) = F(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 HILBERT2:sch 3( A1, A4, A8, A7);

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

        

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

        proof

          let r, s such that

           A13: (M . r) is Permutation of (( SetVal V) . r) & (M . s) is Permutation of (( SetVal V) . s);

          

           A14: (( SetVal V) . (r '&' s)) = [:( SetVal (V,r)), ( SetVal (V,s)):] by Def2;

          ex p9 be Permutation of ( SetVal (V,r)), q9 be Permutation of ( SetVal (V,s)) st p9 = (M . r) & q9 = (M . s) & (M . (r '&' s)) = [:p9, q9:] by A11, A13;

          hence (M . (r '&' s)) is Permutation of (( SetVal V) . (r '&' s)) by A14;

          

           A15: (( SetVal V) . (r => s)) = ( Funcs (( SetVal (V,r)),( SetVal (V,s)))) by Def2;

          ex p9 be Permutation of ( SetVal (V,r)), q9 be Permutation of ( SetVal (V,s)) st p9 = (M . r) & q9 = (M . s) & (M . (r => s)) = (p9 => q9) by A11, A13;

          hence thesis by A15;

        end;

        take M;

        

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

        proof

          let n;

          (M . ( prop n)) = (P . n) & (( SetVal V) . ( prop n)) = (V . n) by A10, Def2;

          hence thesis by Def4;

        end;

        (( SetVal V) . VERUM ) = 1 by Def2;

        then

         A17: P[ VERUM ] by A9;

        

         A18: for p holds P[p] from HILBERT2:sch 2( A17, A16, A12);

        thus M is ManySortedFunction of ( SetVal V), ( SetVal V)

        proof

          let p be object;

          thus thesis by A18;

        end;

        thus (M . VERUM ) = ( id 1) by A9;

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

        let p, q;

        

         A19: (M . p) is Permutation of (( SetVal V) . p) & (M . q) is Permutation of (( SetVal V) . q) by A18;

        then

        consider p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q)) such that

         A20: p9 = (M . p) & q9 = (M . q) and

         A21: (M . (p '&' q)) = [:p9, q9:] by A11;

        take p9, q9;

        thus p9 = (M . p) & q9 = (M . q) & (M . (p '&' q)) = [:p9, q9:] by A20, A21;

        ex p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q)) st p9 = (M . p) & q9 = (M . q) & (M . (p => q)) = (p9 => q9) by A11, A19;

        hence (M . (p => q)) = (p9 => q9) by A20;

      end;

      uniqueness

      proof

        let M1,M2 be ManySortedFunction of ( SetVal V), ( SetVal V) such that

         A22: (M1 . VERUM ) = ( id 1) and

         A23: for n holds (M1 . ( prop n)) = (P . n) and

         A24: for p, q holds ex p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q)) st p9 = (M1 . p) & q9 = (M1 . q) & (M1 . (p '&' q)) = [:p9, q9:] & (M1 . (p => q)) = (p9 => q9) and

         A25: (M2 . VERUM ) = ( id 1) and

         A26: for n holds (M2 . ( prop n)) = (P . n) and

         A27: for p, q holds ex p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q)) st p9 = (M2 . p) & q9 = (M2 . q) & (M2 . (p '&' q)) = [:p9, q9:] & (M2 . (p => q)) = (p9 => q9);

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

        

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

        proof

          let n;

          

          thus (M1 . ( prop n)) = (P . n) by A23

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

        end;

        

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

        proof

          let r, s such that

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

          

           A31: (ex p9 be Permutation of ( SetVal (V,r)), q9 be Permutation of ( SetVal (V,s)) st p9 = (M1 . r) & q9 = (M1 . s) & (M1 . (r '&' s)) = [:p9, q9:] & (M1 . (r => s)) = (p9 => q9)) & ex p9 be Permutation of ( SetVal (V,r)), q9 be Permutation of ( SetVal (V,s)) st p9 = (M2 . r) & q9 = (M2 . s) & (M2 . (r '&' s)) = [:p9, q9:] & (M2 . (r => s)) = (p9 => q9) by A24, A27;

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

          thus thesis by A30, A31;

        end;

        

         A32: P[ VERUM ] by A22, A25;

        for r holds P[r] from HILBERT2:sch 2( A32, A28, A29);

        hence M1 = M2;

      end;

    end

    definition

      let V, P, p;

      :: HILBERT3:def6

      func Perm (P,p) -> Function of ( SetVal (V,p)), ( SetVal (V,p)) equals (( Perm P) . p);

      correctness ;

    end

    theorem :: HILBERT3:33

    

     Th32: ( Perm (P, VERUM )) = ( id ( SetVal (V, VERUM )))

    proof

      

      thus ( Perm (P, VERUM )) = ( id 1) by Def5

      .= ( id ( SetVal (V, VERUM ))) by Def2;

    end;

    theorem :: HILBERT3:34

    ( Perm (P,( prop n))) = (P . n) by Def5;

    theorem :: HILBERT3:35

    

     Th34: ( Perm (P,(p '&' q))) = [:( Perm (P,p)), ( Perm (P,q)):]

    proof

      ex p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q)) st p9 = (( Perm P) . p) & q9 = (( Perm P) . q) & (( Perm P) . (p '&' q)) = [:p9, q9:] & (( Perm P) . (p => q)) = (p9 => q9) by Def5;

      hence thesis;

    end;

    theorem :: HILBERT3:36

    

     Th35: for p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q)) st p9 = ( Perm (P,p)) & q9 = ( Perm (P,q)) holds ( Perm (P,(p => q))) = (p9 => q9)

    proof

      

       A1: ex p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q)) st p9 = (( Perm P) . p) & q9 = (( Perm P) . q) & (( Perm P) . (p '&' q)) = [:p9, q9:] & (( Perm P) . (p => q)) = (p9 => q9) by Def5;

      let p9 be Permutation of ( SetVal (V,p)), q9 be Permutation of ( SetVal (V,q));

      assume p9 = ( Perm (P,p)) & q9 = ( Perm (P,q));

      hence thesis by A1;

    end;

    registration

      let V, P, p;

      cluster ( Perm (P,p)) -> bijective;

      coherence

      proof

        defpred P[ Element of HP-WFF ] means ( Perm (P,$1)) is bijective;

        

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

        proof

          let n;

          ( SetVal (V,( prop n))) = (V . n) & ( Perm (P,( prop n))) = (P . n) by Def2, Def5;

          hence thesis by Def4;

        end;

        

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

        proof

          let r, s;

          assume ( Perm (P,r)) is bijective;

          then

          reconsider r9 = ( Perm (P,r)) as Permutation of ( SetVal (V,r));

          assume ( Perm (P,s)) is bijective;

          then

          reconsider s9 = ( Perm (P,s)) as Permutation of ( SetVal (V,s));

          ( SetVal (V,(r '&' s))) = [:( SetVal (V,r)), ( SetVal (V,s)):] & ( Perm (P,(r '&' s))) = [:r9, s9:] by Def2, Th34;

          hence ( Perm (P,(r '&' s))) is bijective;

          ( SetVal (V,(r => s))) = ( Funcs (( SetVal (V,r)),( SetVal (V,s)))) & ( Perm (P,(r => s))) = (r9 => s9) by Def2, Th35;

          hence thesis;

        end;

        ( Perm (P, VERUM )) = ( id ( SetVal (V, VERUM ))) by Th32;

        then

         A3: P[ VERUM ];

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

        hence thesis;

      end;

    end

    theorem :: HILBERT3:37

    

     Th36: for g be Function of ( SetVal (V,p)), ( SetVal (V,q)) holds (( Perm (P,(p => q))) . g) = ((( Perm (P,q)) * g) * (( Perm (P,p)) " ))

    proof

      let g be Function of ( SetVal (V,p)), ( SetVal (V,q));

      

      thus (( Perm (P,(p => q))) . g) = ((( Perm (P,p)) => ( Perm (P,q))) . g) by Th35

      .= ((( Perm (P,q)) * g) * (( Perm (P,p)) " )) by Def1;

    end;

    theorem :: HILBERT3:38

    

     Th37: for g be Function of ( SetVal (V,p)), ( SetVal (V,q)) holds ((( Perm (P,(p => q))) " ) . g) = (((( Perm (P,q)) " ) * g) * ( Perm (P,p)))

    proof

      let g be Function of ( SetVal (V,p)), ( SetVal (V,q));

      

      thus ((( Perm (P,(p => q))) " ) . g) = (((( Perm (P,p)) => ( Perm (P,q))) " ) . g) by Th35

      .= (((( Perm (P,q)) " ) * g) * ( Perm (P,p))) by Th25;

    end;

    theorem :: HILBERT3:39

    

     Th38: for f,g be Function of ( SetVal (V,p)), ( SetVal (V,q)) st f = (( Perm (P,(p => q))) . g) holds (( Perm (P,q)) * g) = (f * ( Perm (P,p)))

    proof

      let f,g be Function of ( SetVal (V,p)), ( SetVal (V,q)) such that

       A1: f = (( Perm (P,(p => q))) . g);

      

      thus (( Perm (P,q)) * g) = ((( Perm (P,q)) * g) * ( id ( SetVal (V,p)))) by FUNCT_2: 17

      .= ((( Perm (P,q)) * g) * ((( Perm (P,p)) " ) * ( Perm (P,p)))) by FUNCT_2: 61

      .= (((( Perm (P,q)) * g) * (( Perm (P,p)) " )) * ( Perm (P,p))) by RELAT_1: 36

      .= (f * ( Perm (P,p))) by A1, Th36;

    end;

    theorem :: HILBERT3:40

    

     Th39: for V holds for P be Permutation of V holds for x be set st x is_a_fixpoint_of ( Perm (P,p)) holds for f be Function st f is_a_fixpoint_of ( Perm (P,(p => q))) holds (f . x) is_a_fixpoint_of ( Perm (P,q))

    proof

      let V;

      let P be Permutation of V;

      let x be set such that

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

      let f be Function such that

       A2: f is_a_fixpoint_of ( Perm (P,(p => q)));

      ( dom ( Perm (P,(p => q)))) = ( SetVal (V,(p => q))) by FUNCT_2: 52

      .= ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by Def2;

      then

      reconsider g = f as Function of ( SetVal (V,p)), ( SetVal (V,q)) by A2, FUNCT_2: 66;

      set h = (( Perm (P,(p => q))) . f);

      h = ((( Perm (P,q)) * g) * (( Perm (P,p)) " )) by Th36;

      then

      reconsider h as Function of ( SetVal (V,p)), ( SetVal (V,q));

      

       A3: h = f by A2;

      

       A4: x in ( SetVal (V,p)) by A1, FUNCT_2: 52;

      ( dom ( Perm (P,(p => q)))) = ( SetVal (V,(p => q))) by FUNCT_2: 52

      .= ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by Def2;

      then (f . x) in ( SetVal (V,q)) by A4, Th4, A2;

      hence (f . x) in ( dom ( Perm (P,q))) by FUNCT_2: 52;

      

      thus (( Perm (P,q)) . (f . x)) = ((( Perm (P,q)) * g) . x) by A4, FUNCT_2: 15

      .= ((f * ( Perm (P,p))) . x) by A3, Th38

      .= (f . (( Perm (P,p)) . x)) by A4, FUNCT_2: 15

      .= (f . x) by A1;

    end;

    begin

    definition

      let p;

      :: HILBERT3:def7

      attr p is canonical means for V holds ex x be set st for P be Permutation of V holds x is_a_fixpoint_of ( Perm (P,p));

    end

    registration

      cluster VERUM -> canonical;

      coherence

      proof

        let V;

        take 0 ;

        let P be Permutation of V;

        ( SetVal (V, VERUM )) = 1 & 0 in 1 by Def2, CARD_1: 49, TARSKI:def 1;

        hence thesis by Th3, CARD_1: 49;

      end;

    end

    registration

      let p, q;

      cluster (p => (q => p)) -> canonical;

      coherence

      proof

        let V;

        deffunc F( set) = (( SetVal (V,q)) --> $1);

        

         A1: for x be Element of ( SetVal (V,p)) holds F(x) in ( SetVal (V,(q => p)))

        proof

          let x be Element of ( SetVal (V,p));

          (( SetVal (V,q)) --> x) in ( Funcs (( SetVal (V,q)),( SetVal (V,p)))) by FUNCT_2: 8;

          hence thesis by Def2;

        end;

        consider f be Function of ( SetVal (V,p)), ( SetVal (V,(q => p))) such that

         A2: for x be Element of ( SetVal (V,p)) holds (f . x) = F(x) from FUNCT_2:sch 8( A1);

        take f;

        let P be Permutation of V;

        f in ( Funcs (( SetVal (V,p)),( SetVal (V,(q => p))))) by FUNCT_2: 8;

        then f in ( SetVal (V,(p => (q => p)))) by Def2;

        hence f in ( dom ( Perm (P,(p => (q => p))))) by FUNCT_2:def 1;

        now

          let x be Element of ( SetVal (V,p));

          reconsider g = (( SetVal (V,q)) --> ((( Perm (P,p)) " ) . x)) as Function of ( SetVal (V,q)), ( SetVal (V,p));

          x in ( SetVal (V,p));

          then x in ( rng ( Perm (P,p))) by FUNCT_2:def 3;

          then

           A3: ((( Perm (P,p)) " ) . x) in ( dom ( Perm (P,p))) by PARTFUN2: 60;

          

          thus (f . x) = (( SetVal (V,q)) --> x) by A2

          .= (( SetVal (V,q)) --> (( id ( SetVal (V,p))) . x))

          .= (( SetVal (V,q)) --> ((( Perm (P,p)) * (( Perm (P,p)) " )) . x)) by FUNCT_2: 61

          .= (( SetVal (V,q)) --> (( Perm (P,p)) . ((( Perm (P,p)) " ) . x))) by FUNCT_2: 15

          .= (( Perm (P,p)) * (( SetVal (V,q)) --> ((( Perm (P,p)) " ) . x))) by A3, FUNCOP_1: 17

          .= (( Perm (P,p)) * (((( Perm (P,q)) " ) " ( SetVal (V,q))) --> ((( Perm (P,p)) " ) . x))) by FUNCT_2: 40

          .= (( Perm (P,p)) * (g * (( Perm (P,q)) " ))) by FUNCOP_1: 19

          .= ((( Perm (P,p)) * g) * (( Perm (P,q)) " )) by RELAT_1: 36

          .= (( Perm (P,(q => p))) . g) by Th36

          .= (( Perm (P,(q => p))) . (f . ((( Perm (P,p)) " ) . x))) by A2

          .= ((( Perm (P,(q => p))) * f) . ((( Perm (P,p)) " ) . x)) by FUNCT_2: 15

          .= (((( Perm (P,(q => p))) * f) * (( Perm (P,p)) " )) . x) by FUNCT_2: 15;

        end;

        

        hence f = ((( Perm (P,(q => p))) * f) * (( Perm (P,p)) " ))

        .= (( Perm (P,(p => (q => p)))) . f) by Th36;

      end;

      cluster ((p '&' q) => p) -> canonical;

      coherence

      proof

        let V;

        take f = ( pr1 (( SetVal (V,p)),( SetVal (V,q))));

        let P be Permutation of V;

        

         A4: ( dom ( Perm (P,((p '&' q) => p)))) = ( SetVal (V,((p '&' q) => p))) by FUNCT_2:def 1

        .= ( Funcs (( SetVal (V,(p '&' q))),( SetVal (V,p)))) by Def2

        .= ( Funcs ( [:( SetVal (V,p)), ( SetVal (V,q)):],( SetVal (V,p)))) by Def2;

        hence f in ( dom ( Perm (P,((p '&' q) => p)))) by FUNCT_2: 8;

        then f in ( Funcs (( SetVal (V,(p '&' q))),( SetVal (V,p)))) by A4, Def2;

        then

        reconsider F = f as Function of ( SetVal (V,(p '&' q))), ( SetVal (V,p)) by FUNCT_2: 66;

        

        thus (( Perm (P,((p '&' q) => p))) . f) = ((( Perm (P,p)) * F) * (( Perm (P,(p '&' q))) " )) by Th36

        .= ((( Perm (P,p)) * F) * ( [:( Perm (P,p)), ( Perm (P,q)):] " )) by Th34

        .= ((( Perm (P,p)) * F) * [:(( Perm (P,p)) " ), (( Perm (P,q)) " ):]) by FUNCTOR0: 6

        .= (( Perm (P,p)) * (F * [:(( Perm (P,p)) " ), (( Perm (P,q)) " ):])) by RELAT_1: 36

        .= (( Perm (P,p)) * ((( Perm (P,p)) " ) * F)) by Th15

        .= ((( Perm (P,p)) * (( Perm (P,p)) " )) * F) by RELAT_1: 36

        .= (( id ( SetVal (V,p))) * F) by FUNCT_2: 61

        .= f by FUNCT_2: 17;

      end;

      cluster ((p '&' q) => q) -> canonical;

      coherence

      proof

        let V;

        take f = ( pr2 (( SetVal (V,p)),( SetVal (V,q))));

        let P be Permutation of V;

        

         A5: ( dom ( Perm (P,((p '&' q) => q)))) = ( SetVal (V,((p '&' q) => q))) by FUNCT_2:def 1

        .= ( Funcs (( SetVal (V,(p '&' q))),( SetVal (V,q)))) by Def2

        .= ( Funcs ( [:( SetVal (V,p)), ( SetVal (V,q)):],( SetVal (V,q)))) by Def2;

        hence f in ( dom ( Perm (P,((p '&' q) => q)))) by FUNCT_2: 8;

        then f in ( Funcs (( SetVal (V,(p '&' q))),( SetVal (V,q)))) by A5, Def2;

        then

        reconsider F = f as Function of ( SetVal (V,(p '&' q))), ( SetVal (V,q)) by FUNCT_2: 66;

        

        thus (( Perm (P,((p '&' q) => q))) . f) = ((( Perm (P,q)) * F) * (( Perm (P,(p '&' q))) " )) by Th36

        .= ((( Perm (P,q)) * F) * ( [:( Perm (P,p)), ( Perm (P,q)):] " )) by Th34

        .= ((( Perm (P,q)) * F) * [:(( Perm (P,p)) " ), (( Perm (P,q)) " ):]) by FUNCTOR0: 6

        .= (( Perm (P,q)) * (F * [:(( Perm (P,p)) " ), (( Perm (P,q)) " ):])) by RELAT_1: 36

        .= (( Perm (P,q)) * ((( Perm (P,q)) " ) * F)) by Th16

        .= ((( Perm (P,q)) * (( Perm (P,q)) " )) * F) by RELAT_1: 36

        .= (( id ( SetVal (V,q))) * F) by FUNCT_2: 61

        .= f by FUNCT_2: 17;

      end;

      cluster (p => (q => (p '&' q))) -> canonical;

      coherence

      proof

        let V;

        take f = ( curry [:( id ( SetVal (V,p))), ( id ( SetVal (V,q))):]);

        let P be Permutation of V;

        f in ( Funcs (( SetVal (V,p)),( Funcs (( SetVal (V,q)), [:( SetVal (V,p)), ( SetVal (V,q)):])))) by FUNCT_2: 8;

        then f in ( Funcs (( SetVal (V,p)),( Funcs (( SetVal (V,q)),( SetVal (V,(p '&' q))))))) by Def2;

        then

         A6: f in ( Funcs (( SetVal (V,p)),( SetVal (V,(q => (p '&' q)))))) by Def2;

        then

        reconsider F = f as Function of ( SetVal (V,p)), ( SetVal (V,(q => (p '&' q)))) by FUNCT_2: 66;

        f in ( SetVal (V,(p => (q => (p '&' q))))) by A6, Def2;

        hence f in ( dom ( Perm (P,(p => (q => (p '&' q)))))) by FUNCT_2:def 1;

         A7:

        now

          let x be Element of ( SetVal (V,p));

          set fx = (f . x);

          reconsider fx as Function of ( SetVal (V,q)), ( SetVal (V,(p '&' q))) by Def2;

          set Fx = (F . ((( Perm (P,p)) " ) . x));

          Fx in ( SetVal (V,(q => (p '&' q))));

          then Fx in ( Funcs (( SetVal (V,q)),( SetVal (V,(p '&' q))))) by Def2;

          then

          reconsider Fx as Function of ( SetVal (V,q)), ( SetVal (V,(p '&' q))) by FUNCT_2: 66;

          now

            let y be Element of ( SetVal (V,q));

            

            thus (fx . y) = ( [:( id ( SetVal (V,p))), ( id ( SetVal (V,q))):] . (x,y)) by FUNCT_5: 69

            .= [(( id ( SetVal (V,p))) . x), (( id ( SetVal (V,q))) . y)] by FUNCT_3: 75

            .= [(( id ( SetVal (V,p))) . x), ((( Perm (P,q)) * (( Perm (P,q)) " )) . y)] by FUNCT_2: 61

            .= [(( id ( SetVal (V,p))) . x), (( Perm (P,q)) . ((( Perm (P,q)) " ) . y))] by FUNCT_2: 15

            .= [((( Perm (P,p)) * (( Perm (P,p)) " )) . x), (( Perm (P,q)) . ((( Perm (P,q)) " ) . y))] by FUNCT_2: 61

            .= [(( Perm (P,p)) . ((( Perm (P,p)) " ) . x)), (( Perm (P,q)) . ((( Perm (P,q)) " ) . y))] by FUNCT_2: 15

            .= ( [:( Perm (P,p)), ( Perm (P,q)):] . (((( Perm (P,p)) " ) . x),((( Perm (P,q)) " ) . y))) by FUNCT_3: 75

            .= (( Perm (P,(p '&' q))) . [((( Perm (P,p)) " ) . x), ((( Perm (P,q)) " ) . y)]) by Th34

            .= (( Perm (P,(p '&' q))) . [((( Perm (P,p)) " ) . x), (( id ( SetVal (V,q))) . ((( Perm (P,q)) " ) . y))])

            .= (( Perm (P,(p '&' q))) . [(( id ( SetVal (V,p))) . ((( Perm (P,p)) " ) . x)), (( id ( SetVal (V,q))) . ((( Perm (P,q)) " ) . y))])

            .= (( Perm (P,(p '&' q))) . ( [:( id ( SetVal (V,p))), ( id ( SetVal (V,q))):] . (((( Perm (P,p)) " ) . x),((( Perm (P,q)) " ) . y)))) by FUNCT_3: 75

            .= (( Perm (P,(p '&' q))) . (Fx . ((( Perm (P,q)) " ) . y))) by FUNCT_5: 69

            .= ((( Perm (P,(p '&' q))) * Fx) . ((( Perm (P,q)) " ) . y)) by FUNCT_2: 15

            .= (((( Perm (P,(p '&' q))) * Fx) * (( Perm (P,q)) " )) . y) by FUNCT_2: 15;

          end;

          

          hence (f . x) = ((( Perm (P,(p '&' q))) * Fx) * (( Perm (P,q)) " ))

          .= (( Perm (P,(q => (p '&' q)))) . (F . ((( Perm (P,p)) " ) . x))) by Th36

          .= ((( Perm (P,(q => (p '&' q)))) * F) . ((( Perm (P,p)) " ) . x)) by FUNCT_2: 15

          .= (((( Perm (P,(q => (p '&' q)))) * F) * (( Perm (P,p)) " )) . x) by FUNCT_2: 15;

        end;

        

        thus (( Perm (P,(p => (q => (p '&' q))))) . f) = ((( Perm (P,(q => (p '&' q)))) * F) * (( Perm (P,p)) " )) by Th36

        .= f by A7;

      end;

    end

    registration

      let p, q, r;

      cluster ((p => (q => r)) => ((p => q) => (p => r))) -> canonical;

      coherence

      proof

        deffunc G( Function-yielding Function) = ( Frege $1);

        let V;

        

         A1: ( SetVal (V,(p => q))) = ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) & ( SetVal (V,(p => r))) = ( Funcs (( SetVal (V,p)),( SetVal (V,r)))) by Def2;

        

         A2: for x be Element of ( SetVal (V,(p => (q => r)))) holds G(x) in ( SetVal (V,((p => q) => (p => r))))

        proof

          let x be Element of ( SetVal (V,(p => (q => r))));

          x is Element of ( Funcs (( SetVal (V,p)),( SetVal (V,(q => r))))) by Def2;

          then x is Element of ( Funcs (( SetVal (V,p)),( Funcs (( SetVal (V,q)),( SetVal (V,r)))))) by Def2;

          then ( Frege x) is Function of ( SetVal (V,(p => q))), ( SetVal (V,(p => r))) by A1, Th23;

          then ( Frege x) in ( Funcs (( SetVal (V,(p => q))),( SetVal (V,(p => r))))) by FUNCT_2: 8;

          hence ( Frege x) in ( SetVal (V,((p => q) => (p => r)))) by Def2;

        end;

        consider F be Function of ( SetVal (V,(p => (q => r)))), ( SetVal (V,((p => q) => (p => r)))) such that

         A3: for x be Element of ( SetVal (V,(p => (q => r)))) holds (F . x) = G(x) from FUNCT_2:sch 8( A2);

        take F;

        let P be Permutation of V;

        F in ( Funcs (( SetVal (V,(p => (q => r)))),( SetVal (V,((p => q) => (p => r)))))) by FUNCT_2: 8;

        then F in ( SetVal (V,((p => (q => r)) => ((p => q) => (p => r))))) by Def2;

        hence F in ( dom ( Perm (P,((p => (q => r)) => ((p => q) => (p => r)))))) by FUNCT_2:def 1;

        now

          reconsider X = (( Perm (P,(q => r))) " ) as Function of ( SetVal (V,(q => r))), ( SetVal (V,(q => r)));

          let f be Element of ( SetVal (V,(p => (q => r))));

          set Yf = ((( Perm (P,(p => (q => r)))) " ) . f);

          

           A4: ( SetVal (V,(q => r))) = ( Funcs (( SetVal (V,q)),( SetVal (V,r)))) by Def2;

          f in ( SetVal (V,(p => (q => r))));

          then f in ( Funcs (( SetVal (V,p)),( SetVal (V,(q => r))))) by Def2;

          then

          reconsider ff = f as Function of ( SetVal (V,p)), ( SetVal (V,(q => r))) by FUNCT_2: 66;

          Yf = (((( Perm (P,(q => r))) " ) * ff) * ( Perm (P,p))) by Th37;

          then

          reconsider h = ( Frege Yf) as Function-yielding Function of ( SetVal (V,(p => q))), ( SetVal (V,(p => r))) by A1, A4, Th23;

          set M = ((( Perm (P,(p => r))) * h) * (( Perm (P,(p => q))) " ));

          

           A5: ( product ( doms ff)) = ( product (( SetVal (V,p)) --> ( SetVal (V,q)))) by A4, Th5

          .= ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by CARD_3: 11;

          then

           A6: ( product ( doms ff)) = ( SetVal (V,(p => q))) by Def2;

          then

          reconsider M as ManySortedFunction of ( product ( doms f));

          

           A7: for g be Function st g in ( product ( doms f)) holds (M . g) = (f .. g)

          proof

            Yf in ( SetVal (V,(p => (q => r))));

            then Yf in ( Funcs (( SetVal (V,p)),( SetVal (V,(q => r))))) by Def2;

            then Yf is Function of ( SetVal (V,p)), ( Funcs (( SetVal (V,q)),( SetVal (V,r)))) by A4, FUNCT_2: 66;

            

            then

             A8: ( product ( doms Yf)) = ( product (( SetVal (V,p)) --> ( SetVal (V,q)))) by Th5

            .= ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by CARD_3: 11

            .= ( SetVal (V,(p => q))) by Def2;

            reconsider FF = ff as Function of ( SetVal (V,p)), ( Funcs (( SetVal (V,q)),( SetVal (V,r)))) by Def2;

            let g be Function such that

             A9: g in ( product ( doms f));

            reconsider G = g as Function of ( SetVal (V,p)), ( SetVal (V,q)) by A5, A9, FUNCT_2: 66;

            

             L: ( dom FF) = ( SetVal (V,p)) by FUNCT_2:def 1;

            

             L2: ( dom G) = ( SetVal (V,p)) by FUNCT_2:def 1;

            

             A10: ( dom (FF .. G)) = (( dom FF) /\ ( dom G)) by PRALG_1:def 19

            .= ( SetVal (V,p)) by L2, L;

            

             A11: ( rng (FF .. G)) c= ( SetVal (V,r)) by Th20;

            then

            reconsider GG = (FF .. G) as Function of ( SetVal (V,p)), ( SetVal (V,r)) by A10, FUNCT_2:def 1, RELSET_1: 4;

            (FF .. G) is Function of ( SetVal (V,p)), ( SetVal (V,r)) by A10, A11, FUNCT_2:def 1, RELSET_1: 4;

            then (FF .. G) in ( Funcs (( SetVal (V,p)),( SetVal (V,r)))) by FUNCT_2: 8;

            then

             A12: (FF .. G) in ( SetVal (V,(p => r))) by Def2;

            (((( Perm (P,q)) " ) * G) * ( Perm (P,p))) in ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by FUNCT_2: 8;

            then

             A13: (((( Perm (P,q)) " ) * g) * ( Perm (P,p))) in ( product ( doms Yf)) by A8, Def2;

            then

             A14: ((( Perm (P,(p => q))) " ) . G) in ( SetVal (V,(p => q))) by A8, Th37;

            

             B2: ( rng G) c= ( SetVal (V,q)) by RELAT_1:def 19;

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

            

            then ( dom ((( Perm (P,q)) " ) * g)) = ( dom g) by RELAT_1: 27, B2

            .= ( SetVal (V,p)) by L2;

            then

             BB: ( dom (X * FF)) = ( dom ((( Perm (P,q)) " ) * g)) by FUNCT_2:def 1;

            

             A15: X = ((( Perm (P,q)) => ( Perm (P,r))) " ) by Th35

            .= ((( Perm (P,q)) " ) => (( Perm (P,r)) " )) by Th26;

            

             A16: (h . ((( Perm (P,(p => q))) " ) . g)) = (h . (((( Perm (P,q)) " ) * G) * ( Perm (P,p)))) by Th37

            .= (Yf .. (((( Perm (P,q)) " ) * g) * ( Perm (P,p)))) by A13, PRALG_2:def 2

            .= (((X * ff) * ( Perm (P,p))) .. (((( Perm (P,q)) " ) * g) * ( Perm (P,p)))) by Th37

            .= (((X * FF) .. ((( Perm (P,q)) " ) * g)) * ( Perm (P,p))) by Th18, BB

            .= (((( Perm (P,r)) " ) * (FF .. G)) * ( Perm (P,p))) by A15, Th27

            .= ((( Perm (P,(p => r))) " ) . GG) by Th37;

            

            thus (M . g) = ((( Perm (P,(p => r))) * h) . ((( Perm (P,(p => q))) " ) . g)) by A6, A9, FUNCT_2: 15

            .= (( Perm (P,(p => r))) . ((( Perm (P,(p => r))) " ) . GG)) by A14, A16, FUNCT_2: 15

            .= ((( Perm (P,(p => r))) * (( Perm (P,(p => r))) " )) . GG) by A12, FUNCT_2: 15

            .= (( id ( SetVal (V,(p => r)))) . GG) by FUNCT_2: 61

            .= (f .. g) by A12, FUNCT_1: 18;

          end;

          

          thus (F . f) = ( Frege f) by A3

          .= ((( Perm (P,(p => r))) * h) * (( Perm (P,(p => q))) " )) by A7, PRALG_2:def 2

          .= (( Perm (P,((p => q) => (p => r)))) . h) by Th36

          .= (( Perm (P,((p => q) => (p => r)))) . (F . ((( Perm (P,(p => (q => r)))) " ) . f))) by A3

          .= ((( Perm (P,((p => q) => (p => r)))) * F) . ((( Perm (P,(p => (q => r)))) " ) . f)) by FUNCT_2: 15

          .= (((( Perm (P,((p => q) => (p => r)))) * F) * (( Perm (P,(p => (q => r)))) " )) . f) by FUNCT_2: 15;

        end;

        

        hence F = ((( Perm (P,((p => q) => (p => r)))) * F) * (( Perm (P,(p => (q => r)))) " ))

        .= (( Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) . F) by Th36;

      end;

    end

    theorem :: HILBERT3:41

    

     Th40: p is canonical & (p => q) is canonical implies q is canonical

    proof

      assume that

       A1: p is canonical and

       A2: (p => q) is canonical;

      let V;

      consider x be set such that

       A3: for P be Permutation of V holds x is_a_fixpoint_of ( Perm (P,p)) by A1;

      set P = the Permutation of V;

      

       A4: ( dom ( Perm (P,(p => q)))) = ( SetVal (V,(p => q))) by FUNCT_2: 52

      .= ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by Def2;

      consider f be set such that

       A5: for P be Permutation of V holds f is_a_fixpoint_of ( Perm (P,(p => q))) by A2;

      f is_a_fixpoint_of ( Perm (P,(p => q))) by A5;

      then

      reconsider f as Function of ( SetVal (V,p)), ( SetVal (V,q)) by FUNCT_2: 66, A4;

      take (f . x);

      let P be Permutation of V;

      

       A6: f is_a_fixpoint_of ( Perm (P,(p => q))) by A5;

      x is_a_fixpoint_of ( Perm (P,p)) by A3;

      hence thesis by A6, Th39;

    end;

    theorem :: HILBERT3:42

    p in HP_TAUT implies p is canonical

    proof

      set X = { q : q is canonical };

      X c= HP-WFF

      proof

        let x be object;

        assume x in X;

        then ex p st p = x & p is canonical;

        hence thesis;

      end;

      then

      reconsider X as Subset of HP-WFF ;

      X is Hilbert_theory

      proof

        thus VERUM in X;

        let p, q, r;

        thus (p => (q => p)) in X;

        thus ((p => (q => r)) => ((p => q) => (p => r))) in X;

        thus ((p '&' q) => p) in X;

        thus ((p '&' q) => q) in X;

        thus (p => (q => (p '&' q))) in X;

        assume p in X;

        then

         A1: ex s st s = p & s is canonical;

        assume (p => q) in X;

        then ex s st s = (p => q) & s is canonical;

        then q is canonical by A1, Th40;

        hence thesis;

      end;

      then

       A2: HP_TAUT c= X by HILBERT1: 13;

      assume p in HP_TAUT ;

      then p in X by A2;

      then ex q st p = q & q is canonical;

      hence thesis;

    end;

    registration

      cluster canonical for Element of HP-WFF ;

      existence

      proof

        take VERUM ;

        thus thesis;

      end;

    end

    begin

    definition

      let p;

      :: HILBERT3:def8

      attr p is pseudo-canonical means for V holds for P be Permutation of V holds ex x be set st x is_a_fixpoint_of ( Perm (P,p));

    end

    registration

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

      coherence

      proof

        let p;

        assume

         A1: p is canonical;

        let V;

        consider x be set such that

         A2: for P be Permutation of V holds x is_a_fixpoint_of ( Perm (P,p)) by A1;

        let P be Permutation of V;

        take x;

        thus thesis by A2;

      end;

    end

    theorem :: HILBERT3:43

    p is pseudo-canonical & (p => q) is pseudo-canonical implies q is pseudo-canonical

    proof

      assume that

       A1: p is pseudo-canonical and

       A2: (p => q) is pseudo-canonical;

      let V;

      let P be Permutation of V;

      consider x be set such that

       A3: x is_a_fixpoint_of ( Perm (P,p)) by A1;

      consider f be set such that

       A4: f is_a_fixpoint_of ( Perm (P,(p => q))) by A2;

      ( dom ( Perm (P,(p => q)))) = ( SetVal (V,(p => q))) by FUNCT_2: 52

      .= ( Funcs (( SetVal (V,p)),( SetVal (V,q)))) by Def2;

      then

      reconsider f as Function of ( SetVal (V,p)), ( SetVal (V,q)) by FUNCT_2: 66, A4;

      take (f . x);

      thus thesis by A3, A4, Th39;

    end;

    theorem :: HILBERT3:44

    

     Th43: for p, q holds for V holds for P be Permutation of V st (ex f be set st f is_a_fixpoint_of ( Perm (P,p))) & not (ex f be set st f is_a_fixpoint_of ( Perm (P,q))) holds not (p => q) is pseudo-canonical

    proof

      let p, q;

      let V;

      let P be Permutation of V;

      given x be set such that

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

      assume

       A2: for x be set holds not x is_a_fixpoint_of ( Perm (P,q));

      assume (p => q) is pseudo-canonical;

      then

      consider f be set such that

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

      reconsider f as Function by A3;

      (f . x) is_a_fixpoint_of ( Perm (P,q)) by A1, A3, Th39;

      hence contradiction by A2;

    end;

    theorem :: HILBERT3:45

    for a,b be Element of NAT st a <> b holds (((( prop a) => ( prop b)) => ( prop a)) => ( prop a)) is non pseudo-canonical

    proof

      let a,b be Element of NAT such that

       A1: a <> b;

      set A = { (( 0 ,1) --> (i,j)) where i,j be Element of INT : i < j or i is even & i = j }, X = ( product (( 0 ,1) --> ( INT , INT )));

      A c= X

      proof

        let x be object;

        assume x in A;

        then ex i,j be Element of INT st x = (( 0 ,1) --> (i,j)) & (i < j or i is even & i = j);

        hence thesis by Th10;

      end;

      then

      reconsider A as Subset of X;

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

      

       A2: not b in ( dom (a .--> 2)) by A1, FUNCOP_1: 75;

      reconsider p1 as Permutation of 2 by Th14;

      defpred P[ set, set] means ex i be Integer st $1 = i & $2 = (i + 1);

      set V = (( NAT --> INT ) +* (a .--> ( Segm 2)));

      reconsider V as SetValuation;

      

       A3: a in ( dom (a .--> 2)) by FUNCOP_1: 74;

      

       A4: 2 = ((a .--> 2) . a) by FUNCOP_1: 72

      .= (V . a) by A3, FUNCT_4: 13

      .= ( SetVal (V,( prop a))) by Def2;

      

       A5: for e be Element of INT holds ex u be Element of INT st P[e, u]

      proof

        let e be Element of INT ;

        reconsider e as Integer;

        reconsider u = (e + 1) as Element of INT by INT_1:def 2;

        take u;

        thus thesis;

      end;

      consider p0 be Function of INT , INT such that

       A6: for e be Element of INT holds P[e, (p0 . e)] from FUNCT_2:sch 3( A5);

      

       A7: ( dom p0) = INT by FUNCT_2:def 1;

      for y be object holds y in INT iff ex x be object st x in ( dom p0) & y = (p0 . x)

      proof

        let y be object;

        hereby

          assume y in INT ;

          then

          reconsider i = y as Integer;

          reconsider x = (i - 1) as object;

          take x;

          thus x in ( dom p0) by A7, INT_1:def 2;

          then ex j be Integer st x = j & (p0 . x) = (j + 1) by A6, A7;

          hence y = (p0 . x) by XCMPLX_1: 27;

        end;

        given x be object such that

         A8: x in ( dom p0) and

         A9: y = (p0 . x);

        ex i be Integer st x = i & (p0 . x) = (i + 1) by A6, A7, A8;

        hence thesis by A9, INT_1:def 2;

      end;

      then

       A10: ( rng p0) = INT by FUNCT_1:def 3;

      

       A11: p0 is one-to-one

      proof

        let x1,x2 be object;

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

        then

        reconsider I1 = x1, I2 = x2 as Element of INT by FUNCT_2:def 1;

        assume

         A12: (p0 . x1) = (p0 . x2);

        (ex i1 be Integer st I1 = i1 & (p0 . I1) = (i1 + 1)) & ex i2 be Integer st I2 = i2 & (p0 . I2) = (i2 + 1) by A6;

        hence thesis by A12, XCMPLX_1: 2;

      end;

      

       A13: ( SetVal (V,( prop b))) = (V . b) by Def2

      .= (( NAT --> INT ) . b) by A2, FUNCT_4: 11

      .= INT ;

      

       A14: X = ( product (2 --> INT )) by CARD_1: 50, FUNCT_4: 65

      .= ( Funcs (2, INT )) by CARD_3: 11

      .= ( SetVal (V,(( prop a) => ( prop b)))) by A4, A13, Def2;

      then

      reconsider f = ( chi (A,X)) as Function of ( SetVal (V,(( prop a) => ( prop b)))), ( SetVal (V,( prop a))) by A4, CARD_1: 50;

      

       A15: a in ( dom (a .--> p1)) by FUNCOP_1: 74;

      reconsider p0 as Permutation of INT by A11, A10, FUNCT_2: 57;

      set P = (( NAT --> p0) +* (a .--> p1));

      

       A16: ( dom P) = (( dom ( NAT --> p0)) \/ ( dom (a .--> p1))) by FUNCT_4:def 1

      .= (( dom ( NAT --> p0)) \/ {a})

      .= ( NAT \/ {a})

      .= NAT by ZFMISC_1: 40;

      for n holds (P . n) is Permutation of (V . n)

      proof

        let n;

        per cases ;

          suppose

           A17: n = a;

          then n in ( dom (a .--> 2)) by FUNCOP_1: 74;

          

          then

           A18: (V . n) = ((a .--> 2) . a) by A17, FUNCT_4: 13

          .= 2 by FUNCOP_1: 72;

          n in ( dom (a .--> p1)) by A17, FUNCOP_1: 74;

          

          then (P . n) = ((a .--> p1) . a) by A17, FUNCT_4: 13

          .= p1 by FUNCOP_1: 72;

          hence thesis by A18;

        end;

          suppose

           A19: n <> a;

          then not n in ( dom (a .--> 2)) by FUNCOP_1: 75;

          

          then

           A20: (V . n) = (( NAT --> INT ) . n) by FUNCT_4: 11

          .= INT ;

           not n in ( dom (a .--> p1)) by A19, FUNCOP_1: 75;

          

          then (P . n) = (( NAT --> p0) . n) by FUNCT_4: 11

          .= p0;

          hence thesis by A20;

        end;

      end;

      then

      reconsider P as Permutation of V by A16, Def4;

      

       A21: ( Perm (P,( prop a))) = (P . a) by Def5

      .= ((a .--> p1) . a) by A15, FUNCT_4: 13

      .= p1 by FUNCOP_1: 72;

      

       A22: f is_a_fixpoint_of ( Perm (P,((( prop a) => ( prop b)) => ( prop a))))

      proof

        set Q = ( Perm (P,((( prop a) => ( prop b)) => ( prop a))));

        f in ( Funcs (( SetVal (V,(( prop a) => ( prop b)))),( SetVal (V,( prop a))))) by FUNCT_2: 8;

        then f in ( SetVal (V,((( prop a) => ( prop b)) => ( prop a)))) by Def2;

        hence f in ( dom Q) by FUNCT_2:def 1;

        ( rng (( Perm (P,(( prop a) => ( prop b)))) " )) = ( dom ((( Perm (P,(( prop a) => ( prop b)))) " ) " )) by FUNCT_1: 32

        .= X by A14, FUNCT_2:def 1

        .= ( dom f) by FUNCT_2:def 1;

        

        then

         A23: ( dom (f * (( Perm (P,(( prop a) => ( prop b)))) " ))) = ( dom (( Perm (P,(( prop a) => ( prop b)))) " )) by RELAT_1: 27

        .= ( rng ( Perm (P,(( prop a) => ( prop b))))) by FUNCT_1: 32

        .= X by A14, FUNCT_2:def 3

        .= ( dom ( chi ((A ` ),X))) by FUNCT_3:def 3;

        for x be object st x in ( dom ( chi ((A ` ),X))) holds ((f * (( Perm (P,(( prop a) => ( prop b)))) " )) . x) = (( chi ((A ` ),X)) . x)

        proof

          

           A24: ( dom (p0 " )) = INT by A10, FUNCT_1: 32;

          let x be object;

          

           A25: not b in ( dom (a .--> p1)) by A1, FUNCOP_1: 75;

          assume

           A26: x in ( dom ( chi ((A ` ),X)));

          then x in X by FUNCT_3:def 3;

          then x in ( Funcs (( SetVal (V,( prop a))),( SetVal (V,( prop b))))) by A14, Def2;

          then

          reconsider g = x as Function of ( SetVal (V,( prop a))), ( SetVal (V,( prop b))) by FUNCT_2: 66;

          consider i0,j0 be Element of INT such that

           A27: g = (( 0 ,1) --> (i0,j0)) by A4, A13, Th11;

          reconsider i0, j0 as Integer;

          

           A28: (j0 - 1) in ( dom p0) by A7, INT_1:def 2;

          then ex i be Integer st (j0 - 1) = i & (p0 . (j0 - 1)) = (i + 1) by A6, A7;

          then

           A29: (p0 . (j0 - 1)) = j0 by XCMPLX_1: 27;

          

           A30: (i0 - 1) in ( dom p0) by A7, INT_1:def 2;

          then ex i be Integer st (i0 - 1) = i & (p0 . (i0 - 1)) = (i + 1) by A6, A7;

          then (p0 . (i0 - 1)) = i0 by XCMPLX_1: 27;

          then

           A31: ((p0 " ) . i0) = (i0 - 1) by A30, FUNCT_1: 34;

          ( Perm (P,( prop b))) = (P . b) by Def5

          .= (( NAT --> p0) . b) by A25, FUNCT_4: 11

          .= p0;

          

          then

           A32: ((( Perm (P,( prop b))) " ) * g) = (( 0 ,1) --> (((p0 " ) . i0),((p0 " ) . j0))) by A27, A24, Th13

          .= (( 0 ,1) --> ((i0 - 1),(j0 - 1))) by A31, A28, A29, FUNCT_1: 34;

          

           A33: ((f * (( Perm (P,(( prop a) => ( prop b)))) " )) . x) = (f . ((( Perm (P,(( prop a) => ( prop b)))) " ) . x)) by A23, A26, FUNCT_1: 12

          .= (f . (((( Perm (P,( prop b))) " ) * g) * ( Perm (P,( prop a))))) by Th37

          .= (f . (( 0 ,1) --> ((j0 - 1),(i0 - 1)))) by A21, A32, Th12;

          per cases ;

            suppose

             A34: x in A;

            then

            consider i,j be Element of INT such that

             A35: x = (( 0 ,1) --> (i,j)) and

             A36: i < j or i is even & i = j;

            

             A37: i = i0 & j = j0 by A27, A35, Th9;

             A38:

            now

              assume (( 0 ,1) --> ((j0 - 1),(i0 - 1))) in A;

              then

              consider i,j be Element of INT such that

               A39: (( 0 ,1) --> ((j0 - 1),(i0 - 1))) = (( 0 ,1) --> (i,j)) and

               A40: i < j or i is even & i = j;

              

               A41: i = (j0 - 1) & j = (i0 - 1) by A39, Th9;

              per cases by A40;

                suppose i < j;

                hence contradiction by A36, A37, A41, XREAL_1: 9;

              end;

                suppose i is even & i = j;

                hence contradiction by A36, A37, A41, XCMPLX_1: 19;

              end;

            end;

            

             A42: x in ((A ` ) ` ) by A34;

            (j0 - 1) in INT & (i0 - 1) in INT by INT_1:def 2;

            then (( 0 ,1) --> ((j0 - 1),(i0 - 1))) in X by Th10;

            then (( 0 ,1) --> ((j0 - 1),(i0 - 1))) in (X \ A) by A38, XBOOLE_0:def 5;

            

            hence ((f * (( Perm (P,(( prop a) => ( prop b)))) " )) . x) = 0 by A33, FUNCT_3: 37

            .= (( chi ((A ` ),X)) . x) by A42, FUNCT_3: 37;

          end;

            suppose

             A43: not x in A;

            x in X by A27, Th10;

            then

             A44: x in (X \ A) by A43, XBOOLE_0:def 5;

            

             A45: (j0 - 1) is Element of INT by INT_1:def 2;

            

             A46: i0 is odd or i0 <> j0 by A27, A43;

            

             A47: (i0 - 1) is Element of INT by INT_1:def 2;

            

             A48: i0 >= j0 by A27, A43;

            now

              per cases by A48, A46, XXREAL_0: 1;

                suppose i0 > j0;

                then (j0 - 1) < (i0 - 1) by XREAL_1: 9;

                hence (( 0 ,1) --> ((j0 - 1),(i0 - 1))) in A by A45, A47;

              end;

                suppose i0 = j0 & i0 is odd;

                hence (( 0 ,1) --> ((j0 - 1),(i0 - 1))) in A by A45;

              end;

            end;

            

            hence ((f * (( Perm (P,(( prop a) => ( prop b)))) " )) . x) = 1 by A33, FUNCT_3:def 3

            .= (( chi ((A ` ),X)) . x) by A44, FUNCT_3:def 3;

          end;

        end;

        then (f * (( Perm (P,(( prop a) => ( prop b)))) " )) = ( chi ((A ` ),X)) by A23;

        

        hence f = (( Perm (P,( prop a))) * (f * (( Perm (P,(( prop a) => ( prop b)))) " ))) by A21, Th8

        .= ((( Perm (P,( prop a))) * f) * (( Perm (P,(( prop a) => ( prop b)))) " )) by RELAT_1: 36

        .= (Q . f) by Th36;

      end;

      for x be set holds not x is_a_fixpoint_of ( Perm (P,( prop a)))

      proof

        let x be set;

        a in ( dom (a .--> 2)) by FUNCOP_1: 74;

        then (V . a) = ((a .--> 2) . a) by FUNCT_4: 13;

        then

         A49: (V . a) = 2 by FUNCOP_1: 72;

        assume x in ( dom ( Perm (P,( prop a))));

        then x in ( SetVal (V,( prop a))) by FUNCT_2:def 1;

        then x in (V . a) by Def2;

        then x = 0 or x = 1 by A49, CARD_1: 50, TARSKI:def 2;

        hence thesis by A21, FUNCT_4: 63;

      end;

      hence thesis by A22, Th43;

    end;