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
A7: now :: thesis: for x being Element of SetVal (V,p) holds f . x = (((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ")) . x
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;
now :: thesis: for y being Element of SetVal (V,q) holds fx . y = (((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")) . y
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;
hence f . x = ((Perm (P,(p '&' q))) * Fx) * ((Perm (P,q)) ")
.= (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;
thus (Perm (P,(p => (q => (p '&' q))))) . f = ((Perm (P,(q => (p '&' q)))) * F) * ((Perm (P,p)) ") by Th36
.= f by A7 ; :: thesis: verum