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