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;

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

hence
(SetVal (V,p)) --> x = (Perm (P,(p => q))) . ((SetVal (V,p)) --> x)
by A7, FUNCOP_1:11; :: thesis: verum((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;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