let p, q be Element of HP-WFF ; :: thesis: for V being SetValuation
for P being Permutation of V
for x being set st x is_a_fixpoint_of Perm P,p holds
for f being Function st f is_a_fixpoint_of Perm P,(p => q) holds
f . x is_a_fixpoint_of Perm P,q
let V be SetValuation; :: thesis: for P being Permutation of V
for x being set st x is_a_fixpoint_of Perm P,p holds
for f being Function st f is_a_fixpoint_of Perm P,(p => q) holds
f . x is_a_fixpoint_of Perm P,q
let P be Permutation of V; :: thesis: for x being set st x is_a_fixpoint_of Perm P,p holds
for f being Function st f is_a_fixpoint_of Perm P,(p => q) holds
f . x is_a_fixpoint_of Perm P,q
let x be set ; :: thesis: ( x is_a_fixpoint_of Perm P,p implies for f being Function st f is_a_fixpoint_of Perm P,(p => q) holds
f . x is_a_fixpoint_of Perm P,q )
assume A1: x is_a_fixpoint_of Perm P,p ; :: thesis: for f being Function st f is_a_fixpoint_of Perm P,(p => q) holds
f . x is_a_fixpoint_of Perm P,q
let f be Function; :: thesis: ( f is_a_fixpoint_of Perm P,(p => q) implies f . x is_a_fixpoint_of Perm P,q )
assume A2: f is_a_fixpoint_of Perm P,(p => q) ; :: thesis: f . x is_a_fixpoint_of Perm P,q
dom (Perm P,(p => q)) = SetVal V,(p => q) by FUNCT_2:67
.= Funcs (SetVal V,p),(SetVal V,q) by Def2 ;
then f in Funcs (SetVal V,p),(SetVal V,q) by A2, ABIAN:def 3;
then reconsider g = f as Function of (SetVal V,p),(SetVal V,q) by FUNCT_2:121;
set h = (Perm P,(p => q)) . f;
(Perm P,(p => q)) . f = ((Perm P,q) * g) * ((Perm P,p) " ) by Th37;
then reconsider h = (Perm P,(p => q)) . f as Function of (SetVal V,p),(SetVal V,q) ;
A3: h = f by A2, ABIAN:def 3;
dom (Perm P,p) = SetVal V,p by FUNCT_2:67;
then A4: x in SetVal V,p by A1, ABIAN:def 3;
dom (Perm P,(p => q)) = SetVal V,(p => q) by FUNCT_2:67
.= Funcs (SetVal V,p),(SetVal V,q) by Def2 ;
then f in Funcs (SetVal V,p),(SetVal V,q) by A2, ABIAN:def 3;
then f . x in SetVal V,q by A4, Th5;
hence f . x in dom (Perm P,q) by FUNCT_2:67; :: according to ABIAN:def 3 :: thesis: f . x = (Perm P,q) . (f . x)
thus (Perm P,q) . (f . x) = ((Perm P,q) * g) . x by A4, FUNCT_2:21
.= (f * (Perm P,p)) . x by A3, Th39
.= f . ((Perm P,p) . x) by A4, FUNCT_2:21
.= f . x by A1, ABIAN:def 3 ; :: thesis: verum