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