let V be SetValuation; :: thesis: for P being Permutation of V

for p, q being Element of HP-WFF st Perm (P,p) is with_fixpoint & Perm (P,q) is without_fixpoints holds

Perm (P,(p => q)) is without_fixpoints

let P be Permutation of V; :: thesis: for p, q being Element of HP-WFF st Perm (P,p) is with_fixpoint & Perm (P,q) is without_fixpoints holds

Perm (P,(p => q)) is without_fixpoints

let p, q be Element of HP-WFF ; :: thesis: ( Perm (P,p) is with_fixpoint & Perm (P,q) is without_fixpoints implies Perm (P,(p => q)) is without_fixpoints )

given x1 being object such that A1: x1 is_a_fixpoint_of Perm (P,p) ; :: according to ABIAN:def 5 :: thesis: ( not Perm (P,q) is without_fixpoints or Perm (P,(p => q)) is without_fixpoints )

reconsider xx1 = x1 as set by TARSKI:1;

assume A2: for x2 being object holds not x2 is_a_fixpoint_of Perm (P,q) ; :: according to ABIAN:def 5 :: thesis: Perm (P,(p => q)) is without_fixpoints

let x be object ; :: according to ABIAN:def 5 :: thesis: not x is_a_fixpoint_of Perm (P,(p => q))

assume A3: x is_a_fixpoint_of Perm (P,(p => q)) ; :: thesis: contradiction

A4: x in dom (Perm (P,(p => q))) by A3, ABIAN:def 3;

SetVal (V,(p => q)) = Funcs ((SetVal (V,p)),(SetVal (V,q))) by HILBERT3:32;

then consider f being Function such that

A5: x = f and

( dom f = SetVal (V,p) & rng f c= SetVal (V,q) ) by A4, FUNCT_2:def 2;

f . xx1 is_a_fixpoint_of Perm (P,q) by A3, A1, A5, HILBERT3:40;

hence contradiction by A2; :: thesis: verum

for p, q being Element of HP-WFF st Perm (P,p) is with_fixpoint & Perm (P,q) is without_fixpoints holds

Perm (P,(p => q)) is without_fixpoints

let P be Permutation of V; :: thesis: for p, q being Element of HP-WFF st Perm (P,p) is with_fixpoint & Perm (P,q) is without_fixpoints holds

Perm (P,(p => q)) is without_fixpoints

let p, q be Element of HP-WFF ; :: thesis: ( Perm (P,p) is with_fixpoint & Perm (P,q) is without_fixpoints implies Perm (P,(p => q)) is without_fixpoints )

given x1 being object such that A1: x1 is_a_fixpoint_of Perm (P,p) ; :: according to ABIAN:def 5 :: thesis: ( not Perm (P,q) is without_fixpoints or Perm (P,(p => q)) is without_fixpoints )

reconsider xx1 = x1 as set by TARSKI:1;

assume A2: for x2 being object holds not x2 is_a_fixpoint_of Perm (P,q) ; :: according to ABIAN:def 5 :: thesis: Perm (P,(p => q)) is without_fixpoints

let x be object ; :: according to ABIAN:def 5 :: thesis: not x is_a_fixpoint_of Perm (P,(p => q))

assume A3: x is_a_fixpoint_of Perm (P,(p => q)) ; :: thesis: contradiction

A4: x in dom (Perm (P,(p => q))) by A3, ABIAN:def 3;

SetVal (V,(p => q)) = Funcs ((SetVal (V,p)),(SetVal (V,q))) by HILBERT3:32;

then consider f being Function such that

A5: x = f and

( dom f = SetVal (V,p) & rng f c= SetVal (V,q) ) by A4, FUNCT_2:def 2;

f . xx1 is_a_fixpoint_of Perm (P,q) by A3, A1, A5, HILBERT3:40;

hence contradiction by A2; :: thesis: verum