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:52

.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ;

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

set h = (Perm (P,(p => q))) . f;

(Perm (P,(p => q))) . f = ((Perm (P,q)) * g) * ((Perm (P,p)) ") by Th36;

then reconsider h = (Perm (P,(p => q))) . f as Function of (SetVal (V,p)),(SetVal (V,q)) ;

A3: h = f by A2;

A4: x in SetVal (V,p) by A1, FUNCT_2:52;

dom (Perm (P,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52

.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ;

then f . x in SetVal (V,q) by A4, Th4, A2;

hence f . x in dom (Perm (P,q)) by FUNCT_2:52; :: 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:15

.= (f * (Perm (P,p))) . x by A3, Th38

.= f . ((Perm (P,p)) . x) by A4, FUNCT_2:15

.= f . x by A1 ; :: thesis: verum

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:52

.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ;

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

set h = (Perm (P,(p => q))) . f;

(Perm (P,(p => q))) . f = ((Perm (P,q)) * g) * ((Perm (P,p)) ") by Th36;

then reconsider h = (Perm (P,(p => q))) . f as Function of (SetVal (V,p)),(SetVal (V,q)) ;

A3: h = f by A2;

A4: x in SetVal (V,p) by A1, FUNCT_2:52;

dom (Perm (P,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:52

.= Funcs ((SetVal (V,p)),(SetVal (V,q))) by Def2 ;

then f . x in SetVal (V,q) by A4, Th4, A2;

hence f . x in dom (Perm (P,q)) by FUNCT_2:52; :: 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:15

.= (f * (Perm (P,p))) . x by A3, Th38

.= f . ((Perm (P,p)) . x) by A4, FUNCT_2:15

.= f . x by A1 ; :: thesis: verum