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))

take f = pr1 ((SetVal (V,p)),(SetVal (V,q))); :: 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))

A4: dom (Perm (P,((p '&' q) => p))) = SetVal (V,((p '&' q) => p)) by FUNCT_2:def 1

.= Funcs ((SetVal (V,(p '&' q))),(SetVal (V,p))) by Def2

.= Funcs ([:(SetVal (V,p)),(SetVal (V,q)):],(SetVal (V,p))) by Def2 ;

hence f in dom (Perm (P,((p '&' q) => p))) by FUNCT_2:8; :: according to ABIAN:def 3 :: thesis: f = (Perm (P,((p '&' q) => p))) . f

then f in Funcs ((SetVal (V,(p '&' q))),(SetVal (V,p))) by A4, Def2;

then reconsider F = f as Function of (SetVal (V,(p '&' q))),(SetVal (V,p)) by FUNCT_2:66;

thus (Perm (P,((p '&' q) => p))) . f = ((Perm (P,p)) * F) * ((Perm (P,(p '&' q))) ") by Th36

.= ((Perm (P,p)) * F) * ([:(Perm (P,p)),(Perm (P,q)):] ") by Th34

.= ((Perm (P,p)) * F) * [:((Perm (P,p)) "),((Perm (P,q)) "):] by FUNCTOR0:6

.= (Perm (P,p)) * (F * [:((Perm (P,p)) "),((Perm (P,q)) "):]) by RELAT_1:36

.= (Perm (P,p)) * (((Perm (P,p)) ") * F) by Th15

.= ((Perm (P,p)) * ((Perm (P,p)) ")) * F by RELAT_1:36

.= (id (SetVal (V,p))) * F by FUNCT_2:61

.= f by FUNCT_2:17 ; :: thesis: verum

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

take f = pr1 ((SetVal (V,p)),(SetVal (V,q))); :: 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))

A4: dom (Perm (P,((p '&' q) => p))) = SetVal (V,((p '&' q) => p)) by FUNCT_2:def 1

.= Funcs ((SetVal (V,(p '&' q))),(SetVal (V,p))) by Def2

.= Funcs ([:(SetVal (V,p)),(SetVal (V,q)):],(SetVal (V,p))) by Def2 ;

hence f in dom (Perm (P,((p '&' q) => p))) by FUNCT_2:8; :: according to ABIAN:def 3 :: thesis: f = (Perm (P,((p '&' q) => p))) . f

then f in Funcs ((SetVal (V,(p '&' q))),(SetVal (V,p))) by A4, Def2;

then reconsider F = f as Function of (SetVal (V,(p '&' q))),(SetVal (V,p)) by FUNCT_2:66;

thus (Perm (P,((p '&' q) => p))) . f = ((Perm (P,p)) * F) * ((Perm (P,(p '&' q))) ") by Th36

.= ((Perm (P,p)) * F) * ([:(Perm (P,p)),(Perm (P,q)):] ") by Th34

.= ((Perm (P,p)) * F) * [:((Perm (P,p)) "),((Perm (P,q)) "):] by FUNCTOR0:6

.= (Perm (P,p)) * (F * [:((Perm (P,p)) "),((Perm (P,q)) "):]) by RELAT_1:36

.= (Perm (P,p)) * (((Perm (P,p)) ") * F) by Th15

.= ((Perm (P,p)) * ((Perm (P,p)) ")) * F by RELAT_1:36

.= (id (SetVal (V,p))) * F by FUNCT_2:61

.= f by FUNCT_2:17 ; :: thesis: verum