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