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 A1, ABIAN:def 3;
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 A2, A3, FUNCT_2:8; :: 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 A5, FUNCT_2:5;
then A7: dom ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) = SetVal (V,p) by A3, FUNCT_2:92;
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 A4, HILBERT3:def 1;
hence ((Perm (P,(p => q))) . ((SetVal (V,p)) --> x)) . z = ((Perm (P,q)) * ((SetVal (V,p)) --> x)) . (((Perm (P,p)) ") . z) by A6, A8, FUNCT_1:12
.= (Perm (P,q)) . (((SetVal (V,p)) --> x) . (((Perm (P,p)) ") . z)) by A7, A8, FUNCT_2:5, FUNCT_2:15
.= (Perm (P,q)) . x by A7, A8, FUNCT_2:5, FUNCOP_1:7
.= x by A1, ABIAN:def 3 ;
:: thesis: verum
end;
hence (SetVal (V,p)) --> x = (Perm (P,(p => q))) . ((SetVal (V,p)) --> x) by A7, FUNCOP_1:11; :: thesis: verum