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