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;

set P = the Permutation of V;

A4: dom (Perm ( the Permutation of V,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52

.= 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;

f is_a_fixpoint_of Perm ( the Permutation of V,(p => q)) by A5;

then reconsider f = f as Function of (SetVal (V,p)),(SetVal (V,q)) by FUNCT_2:66, A4;

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, Th39; :: thesis: verum

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;

set P = the Permutation of V;

A4: dom (Perm ( the Permutation of V,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52

.= 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;

f is_a_fixpoint_of Perm ( the Permutation of V,(p => q)) by A5;

then reconsider f = f as Function of (SetVal (V,p)),(SetVal (V,q)) by FUNCT_2:66, A4;

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, Th39; :: thesis: verum