let p, q, r be Element of HP-WFF ; :: thesis: (p => (q => r)) => ((p => q) => (p => r)) is canonical
deffunc H₁( Function) -> set = Frege $1;
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₁(x) in SetVal (V,((p => q) => (p => r)))

proof

let x be Element of SetVal (V,(p => (q => r))); :: thesis: H₁(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, Th24;
then Frege x in Funcs ((SetVal (V,(p => q))),(SetVal (V,(p => r)))) by FUNCT_2:11;
hence Frege x in SetVal (V,((p => q) => (p => r))) by Def2; :: thesis: verum

end;

consider F being Function of (SetVal (V,(p => (q => r)))),(SetVal (V,((p => q) => (p => r)))) such that
A3: for x being Element of SetVal (V,(p => (q => r))) holds F . x = H₁(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:11;
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

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:121;
((Perm (P,(p => (q => r)))) ") . f = (((Perm (P,(q => r))) ") * ff) * (Perm (P,p)) by Th38;
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, Th24;
set M = ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ");
A5: product (doms ff) = product ((SetVal (V,p)) --> (SetVal (V,q))) by A4, Th6
.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by CARD_3:20 ;
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

((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:121;
then A8: product (doms (((Perm (P,(p => (q => r)))) ") . f)) = product ((SetVal (V,p)) --> (SetVal (V,q))) by Th6
.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by CARD_3:20
.= 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:121;
dom FF = SetVal (V,p) by FUNCT_2:def 1;
then A10: dom (FF .. G) = SetVal (V,p) by PRALG_1:def 17;
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:11;
FF .. G is Function of (SetVal (V,p)),(SetVal (V,r)) by A10, A11, FUNCT_2:def 1, RELSET_1:11;
then FF .. G in Funcs ((SetVal (V,p)),(SetVal (V,r))) by FUNCT_2:11;
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:11;
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, Th38;
A15: X = ((Perm (P,q)) => (Perm (P,r))) " by Th36
.= ((Perm (P,q)) ") => ((Perm (P,r)) ") by Th27 ;
A16: h . (((Perm (P,(p => q))) ") . g) = h . ((((Perm (P,q)) ") * G) * (Perm (P,p))) by Th38
.= (((Perm (P,(p => (q => r)))) ") . f) .. ((((Perm (P,q)) ") * g) * (Perm (P,p))) by A13, PRALG_2:def 8
.= ((X * ff) * (Perm (P,p))) .. ((((Perm (P,q)) ") * g) * (Perm (P,p))) by Th38
.= ((X * FF) .. (((Perm (P,q)) ") * g)) * (Perm (P,p)) by Th18
.= (((Perm (P,r)) ") * (FF .. G)) * (Perm (P,p)) by A15, Th28
.= ((Perm (P,(p => r))) ") . GG by Th38 ;
thus M . g = ((Perm (P,(p => r))) * h) . (((Perm (P,(p => q))) ") . g) by A6, A9, FUNCT_2:21
.= (Perm (P,(p => r))) . (((Perm (P,(p => r))) ") . GG) by A14, A16, FUNCT_2:21
.= ((Perm (P,(p => r))) * ((Perm (P,(p => r))) ")) . GG by A12, FUNCT_2:21
.= (id (SetVal (V,(p => r)))) . GG by FUNCT_2:88
.= f .. g by A12, FUNCT_1:35 ; :: thesis: verum

end;

thus F . f = Frege f by A3
.= ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ") by A7, PRALG_2:def 8
.= (Perm (P,((p => q) => (p => r)))) . h by Th37
.= (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:21
.= (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f by FUNCT_2:21 ; :: thesis: verum

end;

hence F = ((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ") by FUNCT_2:113
.= (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) . F by Th37 ;
:: thesis: verum