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 H1( set ) -> Element of bool [:(SetVal (V,q)),{p}:] = (SetVal (V,q)) --> p;
A1: for x being Element of SetVal (V,p) holds H1(x) in SetVal (V,(q => p))
proof
let x be Element of SetVal (V,p); :: thesis: H1(x) in SetVal (V,(q => p))
(SetVal (V,q)) --> x in Funcs ((SetVal (V,q)),(SetVal (V,p))) by FUNCT_2:8;
hence H1(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 = H1(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:8;
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 :: thesis: for x being Element of SetVal (V,p) holds f . x = (((Perm (P,(q => p))) * f) * ((Perm (P,p)) ")) . x
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:60;
thus f . x = (SetVal (V,q)) --> x by A2
.= (SetVal (V,q)) --> ((id (SetVal (V,p))) . x)
.= (SetVal (V,q)) --> (((Perm (P,p)) * ((Perm (P,p)) ")) . x) by FUNCT_2:61
.= (SetVal (V,q)) --> ((Perm (P,p)) . (((Perm (P,p)) ") . x)) by FUNCT_2:15
.= (Perm (P,p)) * ((SetVal (V,q)) --> (((Perm (P,p)) ") . x)) by A3, FUNCOP_1:17
.= (Perm (P,p)) * ((((Perm (P,q)) ") " (SetVal (V,q))) --> (((Perm (P,p)) ") . x)) by FUNCT_2:40
.= (Perm (P,p)) * (g * ((Perm (P,q)) ")) by FUNCOP_1:19
.= ((Perm (P,p)) * g) * ((Perm (P,q)) ") by RELAT_1:36
.= (Perm (P,(q => p))) . g by Th36
.= (Perm (P,(q => p))) . (f . (((Perm (P,p)) ") . x)) by A2
.= ((Perm (P,(q => p))) * f) . (((Perm (P,p)) ") . x) by FUNCT_2:15
.= (((Perm (P,(q => p))) * f) * ((Perm (P,p)) ")) . x by FUNCT_2:15 ; :: thesis: verum
end;
hence f = ((Perm (P,(q => p))) * f) * ((Perm (P,p)) ")
.= (Perm (P,(p => (q => p)))) . f by Th36 ;
:: thesis: verum