deffunc H1( Function-yielding Function) -> set = Frege p;
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 => r)) => ((p => q) => (p => r))))
A1: ( SetVal (V,(p => q)) = Funcs ((SetVal (V,p)),(SetVal (V,q))) & SetVal (V,(p => r)) = Funcs ((SetVal (V,p)),(SetVal (V,r))) ) by Def2;
A2: for x being Element of SetVal (V,(p => (q => r))) holds H1(x) in SetVal (V,((p => q) => (p => r)))
proof
let x be Element of SetVal (V,(p => (q => r))); :: thesis: H1(x) in SetVal (V,((p => q) => (p => r)))
x is Element of Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2;
then x is Element of Funcs ((SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,r))))) by Def2;
then Frege x is Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) by A1, Th23;
then Frege x in Funcs ((SetVal (V,(p => q))),(SetVal (V,(p => r)))) by FUNCT_2:8;
hence Frege x in SetVal (V,((p => q) => (p => r))) by Def2; :: thesis: verum
end;
consider F being Function of (SetVal (V,(p => (q => r)))),(SetVal (V,((p => q) => (p => r)))) such that
A3: for x being Element of SetVal (V,(p => (q => r))) holds F . x = H1(x) from FUNCT_2:sch 8(A2);
 take F ; :: thesis: for P being Permutation of V holds F is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r))))
let P be Permutation of V; :: thesis: F is_a_fixpoint_of Perm (P,((p => (q => r)) => ((p => q) => (p => r))))
F in Funcs ((SetVal (V,(p => (q => r)))),(SetVal (V,((p => q) => (p => r))))) by FUNCT_2:8;
then F in SetVal (V,((p => (q => r)) => ((p => q) => (p => r)))) by Def2;
hence F in dom (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) by FUNCT_2:def 1; :: according to ABIAN:def 3 :: thesis: F = (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) . F
now :: thesis: for f being Element of SetVal (V,(p => (q => r))) holds F . f = (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f
reconsider X = (Perm (P,(q => r))) " as Function of (SetVal (V,(q => r))),(SetVal (V,(q => r))) ;
let f be Element of SetVal (V,(p => (q => r))); :: thesis: F . f = (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f
set Yf = ((Perm (P,(p => (q => r)))) ") . f;
A4: SetVal (V,(q => r)) = Funcs ((SetVal (V,q)),(SetVal (V,r))) by Def2;
f in SetVal (V,(p => (q => r))) ;
then f in Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2;
then reconsider ff = f as Function of (SetVal (V,p)),(SetVal (V,(q => r))) by FUNCT_2:66;
((Perm (P,(p => (q => r)))) ") . f = (((Perm (P,(q => r))) ") * ff) * (Perm (P,p)) by Th37;
then reconsider h = Frege (((Perm (P,(p => (q => r)))) ") . f) as Function-yielding Function of (SetVal (V,(p => q))),(SetVal (V,(p => r))) by A1, A4, Th23;
set M = ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ");
A5: product (doms ff) = product ((SetVal (V,p)) --> (SetVal (V,q))) by A4, Th5
.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by CARD_3:11 ;
then A6: product (doms ff) = SetVal (V,(p => q)) by Def2;
then reconsider M = ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ") as ManySortedFunction of product (doms f) ;
A7: for g being Function st g in product (doms f) holds
M . g = f .. g
proof
((Perm (P,(p => (q => r)))) ") . f in SetVal (V,(p => (q => r))) ;
then ((Perm (P,(p => (q => r)))) ") . f in Funcs ((SetVal (V,p)),(SetVal (V,(q => r)))) by Def2;
then ((Perm (P,(p => (q => r)))) ") . f is Function of (SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,r)))) by A4, FUNCT_2:66;
then A8: product (doms (((Perm (P,(p => (q => r)))) ") . f)) = product ((SetVal (V,p)) --> (SetVal (V,q))) by Th5
.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by CARD_3:11
.= SetVal (V,(p => q)) by Def2 ;
reconsider FF = ff as Function of (SetVal (V,p)),(Funcs ((SetVal (V,q)),(SetVal (V,r)))) by Def2;
let g be Function; :: thesis: ( g in product (doms f) implies M . g = f .. g )
assume A9: g in product (doms f) ; :: thesis: M . g = f .. g
reconsider G = g as Function of (SetVal (V,p)),(SetVal (V,q)) by A5, A9, FUNCT_2:66;
L: dom FF = SetVal (V,p) by FUNCT_2:def 1;
L2: dom G = SetVal (V,p) by FUNCT_2:def 1;
A10: dom (FF .. G) = (dom FF) /\ (dom G) by PRALG_1:def 19
.= SetVal (V,p) by L2, L ;
A11: rng (FF .. G) c= SetVal (V,r) by Th20;
then reconsider GG = FF .. G as Function of (SetVal (V,p)),(SetVal (V,r)) by A10, FUNCT_2:def 1, RELSET_1:4;
FF .. G is Function of (SetVal (V,p)),(SetVal (V,r)) by A10, A11, FUNCT_2:def 1, RELSET_1:4;
then FF .. G in Funcs ((SetVal (V,p)),(SetVal (V,r))) by FUNCT_2:8;
then A12: FF .. G in SetVal (V,(p => r)) by Def2;
(((Perm (P,q)) ") * G) * (Perm (P,p)) in Funcs ((SetVal (V,p)),(SetVal (V,q))) by FUNCT_2:8;
then A13: (((Perm (P,q)) ") * g) * (Perm (P,p)) in product (doms (((Perm (P,(p => (q => r)))) ") . f)) by A8, Def2;
then A14: ((Perm (P,(p => q))) ") . G in SetVal (V,(p => q)) by A8, Th37;
B2: rng G c= SetVal (V,q) by RELAT_1:def 19;
dom ((Perm (P,q)) ") = SetVal (V,q) by FUNCT_2:def 1;
then dom (((Perm (P,q)) ") * g) = dom g by RELAT_1:27, B2
.= SetVal (V,p) by L2 ;
then BB: dom (X * FF) = dom (((Perm (P,q)) ") * g) by FUNCT_2:def 1;
A15: X = ((Perm (P,q)) => (Perm (P,r))) " by Th35
.= ((Perm (P,q)) ") => ((Perm (P,r)) ") by Th26 ;
A16: h . (((Perm (P,(p => q))) ") . g) = h . ((((Perm (P,q)) ") * G) * (Perm (P,p))) by Th37
.= (((Perm (P,(p => (q => r)))) ") . f) .. ((((Perm (P,q)) ") * g) * (Perm (P,p))) by A13, PRALG_2:def 2
.= ((X * ff) * (Perm (P,p))) .. ((((Perm (P,q)) ") * g) * (Perm (P,p))) by Th37
.= ((X * FF) .. (((Perm (P,q)) ") * g)) * (Perm (P,p)) by Th18, BB
.= (((Perm (P,r)) ") * (FF .. G)) * (Perm (P,p)) by A15, Th27
.= ((Perm (P,(p => r))) ") . GG by Th37 ;
thus M . g = ((Perm (P,(p => r))) * h) . (((Perm (P,(p => q))) ") . g) by A6, A9, FUNCT_2:15
.= (Perm (P,(p => r))) . (((Perm (P,(p => r))) ") . GG) by A14, A16, FUNCT_2:15
.= ((Perm (P,(p => r))) * ((Perm (P,(p => r))) ")) . GG by A12, FUNCT_2:15
.= (id (SetVal (V,(p => r)))) . GG by FUNCT_2:61
.= f .. g by A12, FUNCT_1:18 ; :: thesis: verum
end;
thus F . f = Frege f by A3
.= ((Perm (P,(p => r))) * h) * ((Perm (P,(p => q))) ") by A7, PRALG_2:def 2
.= (Perm (P,((p => q) => (p => r)))) . h by Th36
.= (Perm (P,((p => q) => (p => r)))) . (F . (((Perm (P,(p => (q => r)))) ") . f)) by A3
.= ((Perm (P,((p => q) => (p => r)))) * F) . (((Perm (P,(p => (q => r)))) ") . f) by FUNCT_2:15
.= (((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")) . f by FUNCT_2:15 ; :: thesis: verum
end;
hence F = ((Perm (P,((p => q) => (p => r)))) * F) * ((Perm (P,(p => (q => r)))) ")
.= (Perm (P,((p => (q => r)) => ((p => q) => (p => r))))) . F by Th36 ;
:: thesis: verum