let p, q be Element of HP-WFF ; :: thesis: (p '&' q) => p 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)
take f = pr1 (SetVal V,p),(SetVal V,q); :: thesis: for P being Permutation of V holds f is_a_fixpoint_of Perm P,((p '&' q) => p)
let P be Permutation of V; :: thesis: f is_a_fixpoint_of Perm P,((p '&' q) => p)
A1: dom (Perm P,((p '&' q) => p)) = SetVal V,((p '&' q) => p) by FUNCT_2:def 1
.= Funcs (SetVal V,(p '&' q)),(SetVal V,p) by Def2
.= Funcs [:(SetVal V,p),(SetVal V,q):],(SetVal V,p) by Def2 ;
hence f in dom (Perm P,((p '&' q) => p)) by FUNCT_2:11; :: according to ABIAN:def 3 :: thesis: f = (Perm P,((p '&' q) => p)) . f
then f in Funcs (SetVal V,(p '&' q)),(SetVal V,p) by A1, Def2;
then reconsider F = f as Function of (SetVal V,(p '&' q)),(SetVal V,p) by FUNCT_2:121;
thus (Perm P,((p '&' q) => p)) . f = ((Perm P,p) * F) * ((Perm P,(p '&' q)) " ) by Th37
.= ((Perm P,p) * F) * ([:(Perm P,p),(Perm P,q):] " ) by Th35
.= ((Perm P,p) * F) * [:((Perm P,p) " ),((Perm P,q) " ):] by FUNCTOR0:7
.= (Perm P,p) * (F * [:((Perm P,p) " ),((Perm P,q) " ):]) by RELAT_1:55
.= (Perm P,p) * (((Perm P,p) " ) * F) by Th15
.= ((Perm P,p) * ((Perm P,p) " )) * F by RELAT_1:55
.= (id (SetVal V,p)) * F by FUNCT_2:88
.= f by FUNCT_2:23 ; :: thesis: verum