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_{1}( set ) -> Element of bool [:(SetVal (V,q)),{p}:] = (SetVal (V,q)) --> p;

A1: for x being Element of SetVal (V,p) holds H_{1}(x) in SetVal (V,(q => p))

A2: for x being Element of SetVal (V,p) holds f . x = H_{1}(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

.= (Perm (P,(p => (q => p)))) . f by Th36 ;

:: thesis: verum

for P being Permutation of V holds x is_a_fixpoint_of Perm (P,(p => (q => p)))

deffunc H

A1: for x being Element of SetVal (V,p) holds H

proof

consider f being Function of (SetVal (V,p)),(SetVal (V,(q => p))) such that
let x be Element of SetVal (V,p); :: thesis: H_{1}(x) in SetVal (V,(q => p))

(SetVal (V,q)) --> x in Funcs ((SetVal (V,q)),(SetVal (V,p))) by FUNCT_2:8;

hence H_{1}(x) in SetVal (V,(q => p))
by Def2; :: thesis: verum

end;(SetVal (V,q)) --> x in Funcs ((SetVal (V,q)),(SetVal (V,p))) by FUNCT_2:8;

hence H

A2: for x being Element of SetVal (V,p) holds f . x = H

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

hence f =
((Perm (P,(q => p))) * f) * ((Perm (P,p)) ")
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;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

.= (Perm (P,(p => (q => p)))) . f by Th36 ;

:: thesis: verum