let p, q be Element of HP-WFF ; :: thesis: p => (q => (p '&' q)) is canonical
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 is Function of (SetVal V,p),(Funcs (SetVal V,q),[:(SetVal V,p),(SetVal V,q):]) by CAT_2:1;
then f in Funcs (SetVal V,p),(Funcs (SetVal V,q),[:(SetVal V,p),(SetVal V,q):]) by FUNCT_2:11;
then f in Funcs (SetVal V,p),(Funcs (SetVal V,q),(SetVal V,(p '&' q))) by Def2;
then A1: f in Funcs (SetVal V,p),(SetVal V,(q => (p '&' q))) by Def2;
then f in SetVal V,(p => (q => (p '&' q))) by 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
reconsider F = f as Function of (SetVal V,p),(SetVal V,(q => (p '&' q))) by A1, FUNCT_2:121;

A2: now

let x be Element of SetVal V,p; :: thesis: f . x = (((Perm P,(q => (p '&' q))) * F) * ((Perm P,p) " )) . x
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:121;
set fx = f . x;
F . x in SetVal V,(q => (p '&' q)) ;
then f . x in Funcs (SetVal V,q),(SetVal V,(p '&' q)) by Def2;
then reconsider fx = f . x as Function of (SetVal V,q),(SetVal V,(p '&' q)) by FUNCT_2:121;

now

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 CAT_2:3
.= [((id (SetVal V,p)) . x),((id (SetVal V,q)) . y)] by FUNCT_3:96
.= [((id (SetVal V,p)) . x),(((Perm P,q) * ((Perm P,q) " )) . y)] by FUNCT_2:88
.= [((id (SetVal V,p)) . x),((Perm P,q) . (((Perm P,q) " ) . y))] by FUNCT_2:21
.= [(((Perm P,p) * ((Perm P,p) " )) . x),((Perm P,q) . (((Perm P,q) " ) . y))] by FUNCT_2:88
.= [((Perm P,p) . (((Perm P,p) " ) . x)),((Perm P,q) . (((Perm P,q) " ) . y))] by FUNCT_2:21
.= [:(Perm P,p),(Perm P,q):] . (((Perm P,p) " ) . x),(((Perm P,q) " ) . y) by FUNCT_3:96
.= (Perm P,(p '&' q)) . [(((Perm P,p) " ) . x),(((Perm P,q) " ) . y)] by Th35
.= (Perm P,(p '&' q)) . [(((Perm P,p) " ) . x),((id (SetVal V,q)) . (((Perm P,q) " ) . y))] by FUNCT_1:35
.= (Perm P,(p '&' q)) . [((id (SetVal V,p)) . (((Perm P,p) " ) . x)),((id (SetVal V,q)) . (((Perm P,q) " ) . y))] by FUNCT_1:35
.= (Perm P,(p '&' q)) . ([:(id (SetVal V,p)),(id (SetVal V,q)):] . (((Perm P,p) " ) . x),(((Perm P,q) " ) . y)) by FUNCT_3:96
.= (Perm P,(p '&' q)) . (Fx . (((Perm P,q) " ) . y)) by CAT_2:3
.= ((Perm P,(p '&' q)) * Fx) . (((Perm P,q) " ) . y) by FUNCT_2:21
.= (((Perm P,(p '&' q)) * Fx) * ((Perm P,q) " )) . y by FUNCT_2:21 ; :: thesis: verum

end;

hence f . x = ((Perm P,(p '&' q)) * Fx) * ((Perm P,q) " ) by FUNCT_2:113
.= (Perm P,(q => (p '&' q))) . (F . (((Perm P,p) " ) . x)) by Th37
.= ((Perm P,(q => (p '&' q))) * F) . (((Perm P,p) " ) . x) by FUNCT_2:21
.= (((Perm P,(q => (p '&' q))) * F) * ((Perm P,p) " )) . x by FUNCT_2:21 ;
:: thesis: verum

end;

thus (Perm P,(p => (q => (p '&' q)))) . f = ((Perm P,(q => (p '&' q))) * F) * ((Perm P,p) " ) by Th37
.= f by A2, FUNCT_2:113 ; :: thesis: verum