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 '&' q))))

take f = curry [:(id (SetVal (V,p))),(id (SetVal (V,q))):]; :: thesis: for P being Permutation of V holds f is_a_fixpoint_of Perm (P,(p => (q => (p '&' q))))

let P be Permutation of V; :: thesis: f is_a_fixpoint_of Perm (P,(p => (q => (p '&' q))))

f in Funcs ((SetVal (V,p)),(Funcs ((SetVal (V,q)),[:(SetVal (V,p)),(SetVal (V,q)):]))) by FUNCT_2:8;

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

then A6: f in Funcs ((SetVal (V,p)),(SetVal (V,(q => (p '&' q))))) by Def2;

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

f in SetVal (V,(p => (q => (p '&' q)))) by A6, Def2;

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

.= f by A7 ; :: thesis: verum

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

take f = curry [:(id (SetVal (V,p))),(id (SetVal (V,q))):]; :: thesis: for P being Permutation of V holds f is_a_fixpoint_of Perm (P,(p => (q => (p '&' q))))

let P be Permutation of V; :: thesis: f is_a_fixpoint_of Perm (P,(p => (q => (p '&' q))))

f in Funcs ((SetVal (V,p)),(Funcs ((SetVal (V,q)),[:(SetVal (V,p)),(SetVal (V,q)):]))) by FUNCT_2:8;

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

then A6: f in Funcs ((SetVal (V,p)),(SetVal (V,(q => (p '&' q))))) by Def2;

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

f in SetVal (V,(p => (q => (p '&' q)))) by A6, Def2;

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

A7: now :: thesis: for x being Element of SetVal (V,p) holds f . x = (((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ")) . x

thus (Perm (P,(p => (q => (p '&' q))))) . f =
((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ")
by Th36
let x be Element of SetVal (V,p); :: thesis: f . x = (((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ")) . x

set fx = f . x;

reconsider fx = f . x as Function of (SetVal (V,q)),(SetVal (V,(p '&' q))) by Def2;

set Fx = F . (((Perm (P,p)) ") . x);

F . (((Perm (P,p)) ") . x) in SetVal (V,(q => (p '&' q))) ;

then F . (((Perm (P,p)) ") . x) in Funcs ((SetVal (V,q)),(SetVal (V,(p '&' q)))) by Def2;

then reconsider Fx = F . (((Perm (P,p)) ") . x) as Function of (SetVal (V,q)),(SetVal (V,(p '&' q))) by FUNCT_2:66;

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

.= ((Perm (P,(q => (p '&' q)))) * F) . (((Perm (P,p)) ") . x) by FUNCT_2:15

.= (((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ")) . x by FUNCT_2:15 ;

:: thesis: verum

end;set fx = f . x;

reconsider fx = f . x as Function of (SetVal (V,q)),(SetVal (V,(p '&' q))) by Def2;

set Fx = F . (((Perm (P,p)) ") . x);

F . (((Perm (P,p)) ") . x) in SetVal (V,(q => (p '&' q))) ;

then F . (((Perm (P,p)) ") . x) in Funcs ((SetVal (V,q)),(SetVal (V,(p '&' q)))) by Def2;

then reconsider Fx = F . (((Perm (P,p)) ") . x) as Function of (SetVal (V,q)),(SetVal (V,(p '&' q))) by FUNCT_2:66;

now :: thesis: for y being Element of SetVal (V,q) holds fx . y = (((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")) . y

hence f . x =
((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")
let y be Element of SetVal (V,q); :: thesis: fx . y = (((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")) . y

thus fx . y = [:(id (SetVal (V,p))),(id (SetVal (V,q))):] . (x,y) by FUNCT_5:69

.= [((id (SetVal (V,p))) . x),((id (SetVal (V,q))) . y)] by FUNCT_3:75

.= [((id (SetVal (V,p))) . x),(((Perm (P,q)) * ((Perm (P,q)) ")) . y)] by FUNCT_2:61

.= [((id (SetVal (V,p))) . x),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:15

.= [(((Perm (P,p)) * ((Perm (P,p)) ")) . x),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:61

.= [((Perm (P,p)) . (((Perm (P,p)) ") . x)),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:15

.= [:(Perm (P,p)),(Perm (P,q)):] . ((((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y)) by FUNCT_3:75

.= (Perm (P,(p '&' q))) . [(((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y)] by Th34

.= (Perm (P,(p '&' q))) . [(((Perm (P,p)) ") . x),((id (SetVal (V,q))) . (((Perm (P,q)) ") . y))]

.= (Perm (P,(p '&' q))) . [((id (SetVal (V,p))) . (((Perm (P,p)) ") . x)),((id (SetVal (V,q))) . (((Perm (P,q)) ") . y))]

.= (Perm (P,(p '&' q))) . ([:(id (SetVal (V,p))),(id (SetVal (V,q))):] . ((((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y))) by FUNCT_3:75

.= (Perm (P,(p '&' q))) . (Fx . (((Perm (P,q)) ") . y)) by FUNCT_5:69

.= ((Perm (P,(p '&' q))) * Fx) . (((Perm (P,q)) ") . y) by FUNCT_2:15

.= (((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")) . y by FUNCT_2:15 ; :: thesis: verum

end;thus fx . y = [:(id (SetVal (V,p))),(id (SetVal (V,q))):] . (x,y) by FUNCT_5:69

.= [((id (SetVal (V,p))) . x),((id (SetVal (V,q))) . y)] by FUNCT_3:75

.= [((id (SetVal (V,p))) . x),(((Perm (P,q)) * ((Perm (P,q)) ")) . y)] by FUNCT_2:61

.= [((id (SetVal (V,p))) . x),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:15

.= [(((Perm (P,p)) * ((Perm (P,p)) ")) . x),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:61

.= [((Perm (P,p)) . (((Perm (P,p)) ") . x)),((Perm (P,q)) . (((Perm (P,q)) ") . y))] by FUNCT_2:15

.= [:(Perm (P,p)),(Perm (P,q)):] . ((((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y)) by FUNCT_3:75

.= (Perm (P,(p '&' q))) . [(((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y)] by Th34

.= (Perm (P,(p '&' q))) . [(((Perm (P,p)) ") . x),((id (SetVal (V,q))) . (((Perm (P,q)) ") . y))]

.= (Perm (P,(p '&' q))) . [((id (SetVal (V,p))) . (((Perm (P,p)) ") . x)),((id (SetVal (V,q))) . (((Perm (P,q)) ") . y))]

.= (Perm (P,(p '&' q))) . ([:(id (SetVal (V,p))),(id (SetVal (V,q))):] . ((((Perm (P,p)) ") . x),(((Perm (P,q)) ") . y))) by FUNCT_3:75

.= (Perm (P,(p '&' q))) . (Fx . (((Perm (P,q)) ") . y)) by FUNCT_5:69

.= ((Perm (P,(p '&' q))) * Fx) . (((Perm (P,q)) ") . y) by FUNCT_2:15

.= (((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")) . y by FUNCT_2:15 ; :: thesis: verum

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

.= ((Perm (P,(q => (p '&' q)))) * F) . (((Perm (P,p)) ") . x) by FUNCT_2:15

.= (((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ")) . x by FUNCT_2:15 ;

:: thesis: verum

.= f by A7 ; :: thesis: verum