let x be set ; :: thesis: for V being SetValuation
for P being Permutation of V
for p, q being Element of HP-WFF st x is_a_fixpoint_of Perm (P,q) holds
(SetVal (V,p)) --> x is_a_fixpoint_of Perm (P,(p => q))

let V be SetValuation; :: thesis: for P being Permutation of V
for p, q being Element of HP-WFF st x is_a_fixpoint_of Perm (P,q) holds
(SetVal (V,p)) --> x is_a_fixpoint_of Perm (P,(p => q))

let P be Permutation of V; :: thesis: for p, q being Element of HP-WFF st x is_a_fixpoint_of Perm (P,q) holds
(SetVal (V,p)) --> x is_a_fixpoint_of Perm (P,(p => q))

let p, q be Element of HP-WFF ; :: thesis: ( x is_a_fixpoint_of Perm (P,q) implies (SetVal (V,p)) --> x is_a_fixpoint_of Perm (P,(p => q)) )
assume A1: x is_a_fixpoint_of Perm (P,q) ; :: thesis: (SetVal (V,p)) --> x is_a_fixpoint_of Perm (P,(p => q))
set F = (SetVal (V,p)) --> x;
A2: dom (Perm (P,(p => q))) = SetVal (V,(p => q)) by FUNCT_2:def 1;
A3: SetVal (V,(p => q)) = Funcs ((SetVal (V,p)),(SetVal (V,q))) by HILBERT3:32;
x in dom (Perm (P,q)) by ;
then A4: (SetVal (V,p)) --> x is Function of (SetVal (V,p)),(SetVal (V,q)) by FUNCOP_1:46;
hence A5: (SetVal (V,p)) --> x in dom (Perm (P,(p => q))) by ; :: according to ABIAN:def 3 :: thesis: (SetVal (V,p)) --> x = (Perm (P,(p => q))) . ((SetVal (V,p)) --> x)
A6: Perm (P,(p => q)) = (Perm (P,p)) => (Perm (P,q)) by HILBERT3:36;
(Perm (P,(p => q))) . ((SetVal (V,p)) --> x) in SetVal (V,(p => q)) by ;
then A7: dom ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) = SetVal (V,p) by ;
now :: thesis: for z being object st z in dom ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) holds
((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) . z = x
let z be object ; :: thesis: ( z in dom ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) implies ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) . z = x )
assume A8: z in dom ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) ; :: thesis: ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) . z = x
((Perm (P,p)) => (Perm (P,q))) . ((SetVal (V,p)) --> x) = ((Perm (P,q)) * ((SetVal (V,p)) --> x)) * ((Perm (P,p)) ") by ;
hence ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) . z = ((Perm (P,q)) * ((SetVal (V,p)) --> x)) . (((Perm (P,p)) ") . z) by
.= (Perm (P,q)) . (((SetVal (V,p)) --> x) . (((Perm (P,p)) ") . z)) by
.= (Perm (P,q)) . x by
.= x by ;
:: thesis: verum
end;
hence (SetVal (V,p)) --> x = (Perm (P,(p => q))) . ((SetVal (V,p)) --> x) by ; :: thesis: verum