let p, q be Element of HP-WFF ; :: thesis: ( p is canonical & p => q is canonical implies q is canonical )
assume that
A1: p is canonical and
A2: p => q is canonical ; :: thesis: 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,q
consider x being set such that
A3: for P being Permutation of V holds x is_a_fixpoint_of Perm P,p by A1, Def7;
consider P being Permutation of V;
A4: dom (Perm P,(p => q)) = SetVal V,(p => q) by FUNCT_2:67
.= Funcs (SetVal V,p),(SetVal V,q) by Def2 ;
consider f being set such that
A5: for P being Permutation of V holds f is_a_fixpoint_of Perm P,(p => q) by A2, Def7;
f is_a_fixpoint_of Perm P,(p => q) by A5;
then f in Funcs (SetVal V,p),(SetVal V,q) by A4, ABIAN:def 3;
then reconsider f = f as Function of (SetVal V,p),(SetVal V,q) by FUNCT_2:121;
take f . x ; :: thesis: for P being Permutation of V holds f . x is_a_fixpoint_of Perm P,q
let P be Permutation of V; :: thesis: f . x is_a_fixpoint_of Perm P,q
A6: f is_a_fixpoint_of Perm P,(p => q) by A5;
x is_a_fixpoint_of Perm P,p by A3;
hence f . x is_a_fixpoint_of Perm P,q by A6, Th40; :: thesis: verum