let p, q be Element of HP-WFF ; :: thesis: ( p is pseudo-canonical & p => q is pseudo-canonical implies q is pseudo-canonical )
assume that
A1: p is pseudo-canonical and
A2: p => q is pseudo-canonical ; :: thesis: q is pseudo-canonical
let V be SetValuation; :: according to HILBERT3:def 8 :: thesis: for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm (P,q)
let P be Permutation of V; :: thesis: ex x being set st x is_a_fixpoint_of Perm (P,q)
consider x being set such that
A3: x is_a_fixpoint_of Perm (P,p) by A1;
consider f being set such that
A4: f is_a_fixpoint_of Perm (P,(p => q)) by A2;
dom (Perm (P,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52
.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ;
then reconsider f = f as Function of (SetVal (V,p)),(SetVal (V,q)) by FUNCT_2:66, A4;
take f . x ; :: thesis: f . x is_a_fixpoint_of Perm (P,q)
thus f . x is_a_fixpoint_of Perm (P,q) by A3, A4, Th39; :: thesis: verum