deffunc H_{1}( Function-yielding Function) -> set = Frege p;

let V be SetValuation; :: according to HILBERT3:def 7 :: thesis: ex x being set st

for P being Permutation of V holds x is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r))))

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 being Element of SetVal (V,(p => (q => r))) holds H_{1}(x) in SetVal (V,((p => q) => (p => r)))

A3: for x being Element of SetVal (V,(p => (q => r))) holds F . x = H_{1}(x)
from FUNCT_2:sch 8(A2);

take F ; :: thesis: for P being Permutation of V holds F is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r))))

let P be Permutation of V; :: thesis: F is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r))))

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; :: according to ABIAN:def 3 :: thesis: F = (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) . F

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

:: thesis: verum

let V be SetValuation; :: according to HILBERT3:def 7 :: thesis: ex x being set st

for P being Permutation of V holds x is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r))))

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 being Element of SetVal (V,(p => (q => r))) holds H

proof

consider F being Function of (SetVal (V,(p => (q => r)))),(SetVal (V,((p => q) => (p => r)))) such that
let x be Element of SetVal (V,(p => (q => r))); :: thesis: H_{1}(x) in SetVal (V,((p => q) => (p => 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; :: thesis: verum

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

A3: for x being Element of SetVal (V,(p => (q => r))) holds F . x = H

take F ; :: thesis: for P being Permutation of V holds F is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r))))

let P be Permutation of V; :: thesis: F is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r))))

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; :: according to ABIAN:def 3 :: thesis: F = (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) . F

now :: thesis: for f being Element of SetVal (V,(p => (q => r))) holds F . f = (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f

hence F =
((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")
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))); :: thesis: F . f = (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f

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;

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

then reconsider h = Frege (((Perm (P,(p => (q => r)))) ") . f) 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 = ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ") as ManySortedFunction of product (doms f) ;

A7: for g being Function st g in product (doms f) holds

M . g = f .. g

.= ((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 ; :: thesis: verum

end;let f be Element of SetVal (V,(p => (q => r))); :: thesis: F . f = (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f

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;

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

then reconsider h = Frege (((Perm (P,(p => (q => r)))) ") . f) 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 = ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ") as ManySortedFunction of product (doms f) ;

A7: for g being Function st g in product (doms f) holds

M . g = f .. g

proof

thus F . f =
Frege f
by A3
((Perm (P,(p => (q => r)))) ") . f in SetVal (V,(p => (q => r)))
;

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

then ((Perm (P,(p => (q => r)))) ") . f is Function of (SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,r)))) by A4, FUNCT_2:66;

then A8: product (doms (((Perm (P,(p => (q => r)))) ") . f)) = 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; :: thesis: ( g in product (doms f) implies M . g = f .. g )

assume A9: g in product (doms f) ; :: thesis: M . g = f .. g

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 (((Perm (P,(p => (q => r)))) ") . f)) 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

.= (((Perm (P,(p => (q => r)))) ") . f) .. ((((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 ; :: thesis: verum

end;then ((Perm (P,(p => (q => r)))) ") . f in Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2;

then ((Perm (P,(p => (q => r)))) ") . f is Function of (SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,r)))) by A4, FUNCT_2:66;

then A8: product (doms (((Perm (P,(p => (q => r)))) ") . f)) = 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; :: thesis: ( g in product (doms f) implies M . g = f .. g )

assume A9: g in product (doms f) ; :: thesis: M . g = f .. g

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 (((Perm (P,(p => (q => r)))) ") . f)) 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

.= (((Perm (P,(p => (q => r)))) ") . f) .. ((((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 ; :: thesis: verum

.= ((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 ; :: thesis: verum

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

:: thesis: verum