let p, q be Element of HP-WFF ; :: thesis: p => (q => p) is canonical
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 => p)))
deffunc H₁( set ) -> Element of bool [:(SetVal (V,q)),{$1}:] = (SetVal (V,q)) --> $1;
A1: for x being Element of SetVal (V,p) holds H₁(x) in SetVal (V,(q => p))

proof

let x be Element of SetVal (V,p); :: thesis: H₁(x) in SetVal (V,(q => p))
(SetVal (V,q)) --> x in Funcs ((SetVal (V,q)),(SetVal (V,p))) by FUNCT_2:11;
hence H₁(x) in SetVal (V,(q => p)) by Def2; :: thesis: verum

end;

consider f being Function of (SetVal (V,p)),(SetVal (V,(q => p))) such that
A2: for x being Element of SetVal (V,p) holds f . x = H₁(x) from FUNCT_2:sch 8(A1);
take f ; :: thesis: for P being Permutation of V holds f is_a_fixpoint_of Perm (P,(p => (q => p)))
let P be Permutation of V; :: thesis: f is_a_fixpoint_of Perm (P,(p => (q => p)))
f in Funcs ((SetVal (V,p)),(SetVal (V,(q => p)))) by FUNCT_2:11;
then f in SetVal (V,(p => (q => p))) by Def2;
hence f in dom (Perm (P,(p => (q => p)))) by FUNCT_2:def 1; :: according to ABIAN:def 3 :: thesis: f = (Perm (P,(p => (q => p)))) . f

now

let x be Element of SetVal (V,p); :: thesis: f . x = (((Perm (P,(q => p))) * f) * ((Perm (P,p)) ")) . x
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:79;
thus f . x = (SetVal (V,q)) --> x by A2
.= (SetVal (V,q)) --> ((id (SetVal (V,p))) . x) by FUNCT_1:34
.= (SetVal (V,q)) --> (((Perm (P,p)) * ((Perm (P,p)) ")) . x) by FUNCT_2:88
.= (SetVal (V,q)) --> ((Perm (P,p)) . (((Perm (P,p)) ") . x)) by FUNCT_2:21
.= (Perm (P,p)) * ((SetVal (V,q)) --> (((Perm (P,p)) ") . x)) by A3, FUNCOP_1:23
.= (Perm (P,p)) * ((((Perm (P,q)) ") " (SetVal (V,q))) --> (((Perm (P,p)) ") . x)) by FUNCT_2:48
.= (Perm (P,p)) * (g * ((Perm (P,q)) ")) by FUNCOP_1:25
.= ((Perm (P,p)) * g) * ((Perm (P,q)) ") by RELAT_1:55
.= (Perm (P,(q => p))) . g by Th37
.= (Perm (P,(q => p))) . (f . (((Perm (P,p)) ") . x)) by A2
.= ((Perm (P,(q => p))) * f) . (((Perm (P,p)) ") . x) by FUNCT_2:21
.= (((Perm (P,(q => p))) * f) * ((Perm (P,p)) ")) . x by FUNCT_2:21 ; :: thesis: verum

end;

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