let V be SetValuation; HILBERT3:def 7 ex x being set st
for P being Permutation of V holds x is_a_fixpoint_of Perm (P,((p '&' q) => q))
take f = pr2 ((SetVal (V,p)),(SetVal (V,q))); for P being Permutation of V holds f is_a_fixpoint_of Perm (P,((p '&' q) => q))
let P be Permutation of V; f is_a_fixpoint_of Perm (P,((p '&' q) => q))
A5: dom (Perm (P,((p '&' q) => q))) =
SetVal (V,((p '&' q) => q))
by FUNCT_2:def 1
.=
Funcs ((SetVal (V,(p '&' q))),(SetVal (V,q)))
by Def2
.=
Funcs ([:(SetVal (V,p)),(SetVal (V,q)):],(SetVal (V,q)))
by Def2
;
hence
f in dom (Perm (P,((p '&' q) => q)))
by FUNCT_2:8; ABIAN:def 3 f = (Perm (P,((p '&' q) => q))) . f
then
f in Funcs ((SetVal (V,(p '&' q))),(SetVal (V,q)))
by A5, Def2;
then reconsider F = f as Function of (SetVal (V,(p '&' q))),(SetVal (V,q)) by FUNCT_2:66;
thus (Perm (P,((p '&' q) => q))) . f =
((Perm (P,q)) * F) * ((Perm (P,(p '&' q))) ")
by Th36
.=
((Perm (P,q)) * F) * ([:(Perm (P,p)),(Perm (P,q)):] ")
by Th34
.=
((Perm (P,q)) * F) * [:((Perm (P,p)) "),((Perm (P,q)) "):]
by FUNCTOR0:6
.=
(Perm (P,q)) * (F * [:((Perm (P,p)) "),((Perm (P,q)) "):])
by RELAT_1:36
.=
(Perm (P,q)) * (((Perm (P,q)) ") * F)
by Th16
.=
((Perm (P,q)) * ((Perm (P,q)) ")) * F
by RELAT_1:36
.=
(id (SetVal (V,q))) * F
by FUNCT_2:61
.=
f
by FUNCT_2:17
; verum