defpred S₁[ set , set ] means ex i being Integer st
( $1 = i & $2 = i + 1 );
A1: for e being Element of INT ex u being Element of INT st S₁[e,u]

proof

let e be Element of INT ; :: thesis: ex u being Element of INT st S₁[e,u]
reconsider e = e as Integer ;
reconsider u = e + 1 as Element of INT by INT_1:def 2;
take u ; :: thesis: S₁[e,u]
thus S₁[e,u] ; :: thesis: verum

end;

consider p0 being Function of INT ,INT such that
A2: for e being Element of INT holds S₁[e,p0 . e] from FUNCT_2:sch 3(A1);
A3: dom p0 = INT by FUNCT_2:def 1;
A4: p0 is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 p0 or not x2 in proj1 p0 or not p0 . x1 = p0 . x2 or x1 = x2 )
assume ( x1 in dom p0 & x2 in dom p0 ) ; :: thesis: ( not p0 . x1 = p0 . x2 or x1 = x2 )
then reconsider I1 = x1, I2 = x2 as Element of INT by FUNCT_2:def 1;
consider i1 being Integer such that
A5: ( I1 = i1 & p0 . I1 = i1 + 1 ) by A2;
consider i2 being Integer such that
A6: ( I2 = i2 & p0 . I2 = i2 + 1 ) by A2;
assume p0 . x1 = p0 . x2 ; :: thesis: x1 = x2
hence x1 = x2 by A5, A6, XCMPLX_1:2; :: thesis: verum

end;

for y being set holds
( y in INT iff ex x being set st
( x in dom p0 & y = p0 . x ) )

proof

let y be set ; :: thesis: ( y in INT iff ex x being set st
( x in dom p0 & y = p0 . x ) )

hereby :: thesis: ( ex x being set st
( x in dom p0 & y = p0 . x ) implies y in INT )

assume y in INT ; :: thesis: ex x being set st
( x in dom p0 & y = p0 . x )
then reconsider i = y as Integer ;
reconsider x = i - 1 as set ;
take x = x; :: thesis: ( x in dom p0 & y = p0 . x )
thus x in dom p0 by A3, INT_1:def 2; :: thesis: y = p0 . x
then ex j being Integer st
( x = j & p0 . x = j + 1 ) by A2, A3;
hence y = p0 . x by XCMPLX_1:27; :: thesis: verum

end;

given x being set such that A7: x in dom p0 and
A8: y = p0 . x ; :: thesis: y in INT
ex i being Integer st
( x = i & p0 . x = i + 1 ) by A2, A3, A7;
hence y in INT by A8, INT_1:def 2; :: thesis: verum

end;

then A9: rng p0 = INT by FUNCT_1:def 5;
then reconsider p0 = p0 as Permutation of INT by A4, FUNCT_2:83;
set p1 = 0 ,1 --> 1,0 ;
A10: ( dom (0 ,1 --> 1,0 ) = 2 & rng (0 ,1 --> 1,0 ) = 2 ) by CARD_1:88, FUNCT_4:65, FUNCT_4:67;
X: 0 ,1 --> 1,0 is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 (0 ,1 --> 1,0 ) or not x2 in proj1 (0 ,1 --> 1,0 ) or not (0 ,1 --> 1,0 ) . x1 = (0 ,1 --> 1,0 ) . x2 or x1 = x2 )
assume ( x1 in dom (0 ,1 --> 1,0 ) & x2 in dom (0 ,1 --> 1,0 ) ) ; :: thesis: ( not (0 ,1 --> 1,0 ) . x1 = (0 ,1 --> 1,0 ) . x2 or x1 = x2 )
then A11: ( ( x1 = 0 or x1 = 1 ) & ( x2 = 0 or x2 = 1 ) ) by A10, CARD_1:88, TARSKI:def 2;
( (0 ,1 --> 1,0 ) . 0 = 1 & (0 ,1 --> 1,0 ) . 1 = 0 ) by FUNCT_4:66;
hence ( not (0 ,1 --> 1,0 ) . x1 = (0 ,1 --> 1,0 ) . x2 or x1 = x2 ) by A11; :: thesis: verum

end;

0 ,1 --> 1,0 is Function of 2,2 by A10, FUNCT_2:def 1, RELSET_1:11;
then reconsider p1 = 0 ,1 --> 1,0 as Permutation of 2 by A10, X, FUNCT_2:83;
set V = (NAT --> INT ) +* (0 .--> 2);
dom ((NAT --> INT ) +* (0 .--> 2)) = (dom (NAT --> INT )) \/ (dom (0 .--> 2)) by FUNCT_4:def 1
.= (dom (NAT --> INT )) \/ {0 } by FUNCOP_1:19
.= NAT \/ {0 } by FUNCOP_1:19
.= NAT by ZFMISC_1:46 ;
then reconsider V = (NAT --> INT ) +* (0 .--> 2) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
reconsider V = V as SetValuation ;
set P = (NAT --> p0) +* (0 .--> p1);
A13: dom ((NAT --> p0) +* (0 .--> p1)) = (dom (NAT --> p0)) \/ (dom (0 .--> p1)) by FUNCT_4:def 1
.= (dom (NAT --> p0)) \/ {0 } by FUNCOP_1:19
.= NAT \/ {0 } by FUNCOP_1:19
.= NAT by ZFMISC_1:46 ;
for n being Element of NAT holds ((NAT --> p0) +* (0 .--> p1)) . n is Permutation of (V . n)

proof

let n be Element of NAT ; :: thesis: ((NAT --> p0) +* (0 .--> p1)) . n is Permutation of (V . n)

per cases ( n = 0 or n <> 0 ) ;

suppose A14: n = 0 ; :: thesis: ((NAT --> p0) +* (0 .--> p1)) . n is Permutation of (V . n)

then n in dom (0 .--> p1) by FUNCOP_1:89;
then A16: ((NAT --> p0) +* (0 .--> p1)) . n = (0 .--> p1) . 0 by A14, FUNCT_4:14
.= p1 by FUNCOP_1:87 ;
n in dom (0 .--> 2) by A14, FUNCOP_1:89;
then V . n = (0 .--> 2) . 0 by A14, FUNCT_4:14
.= 2 by FUNCOP_1:87 ;
hence ((NAT --> p0) +* (0 .--> p1)) . n is Permutation of (V . n) by A16; :: thesis: verum

end;

suppose S: n <> 0 ; :: thesis: ((NAT --> p0) +* (0 .--> p1)) . n is Permutation of (V . n)

then not n in dom (0 .--> p1) by FUNCOP_1:90;
then A18: ((NAT --> p0) +* (0 .--> p1)) . n = (NAT --> p0) . n by FUNCT_4:12
.= p0 by FUNCOP_1:13 ;
not n in dom (0 .--> 2) by S, FUNCOP_1:90;
then V . n = (NAT --> INT ) . n by FUNCT_4:12
.= INT by FUNCOP_1:13 ;
hence ((NAT --> p0) +* (0 .--> p1)) . n is Permutation of (V . n) by A18; :: thesis: verum

end;

end;

end;

then reconsider P = (NAT --> p0) +* (0 .--> p1) as Permutation of V by A13, Def4;
set A = { (0 ,1 --> i,j) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } ;
set X = product (0 ,1 --> INT ,INT );
{ (0 ,1 --> i,j) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } c= product (0 ,1 --> INT ,INT )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (0 ,1 --> i,j) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } or x in product (0 ,1 --> INT ,INT ) )
assume x in { (0 ,1 --> i,j) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } ; :: thesis: x in product (0 ,1 --> INT ,INT )
then consider i, j being Element of INT such that
A19: x = 0 ,1 --> i,j and
( i < j or ( i is even & i = j ) ) ;
thus x in product (0 ,1 --> INT ,INT ) by A19, Th11; :: thesis: verum

end;

then reconsider A = { (0 ,1 --> i,j) where i, j is Element of INT : ( i < j or ( i is even & i = j ) ) } as Subset of (product (0 ,1 --> INT ,INT )) ;
A21: 0 in dom (0 .--> 2) by FUNCOP_1:89;
A22: 2 = (0 .--> 2) . 0 by FUNCOP_1:87
.= V . 0 by A21, FUNCT_4:14
.= SetVal V,(prop 0 ) by Def2 ;
A23: not 1 in dom (0 .--> 2) by FUNCOP_1:90;
A24: SetVal V,(prop 1) = V . 1 by Def2
.= (NAT --> INT ) . 1 by A23, FUNCT_4:12
.= INT by FUNCOP_1:13 ;
A25: product (0 ,1 --> INT ,INT ) = product (2 --> INT ) by CARD_1:88, FUNCT_4:68
.= Funcs 2,INT by CARD_3:20
.= SetVal V,((prop 0 ) => (prop 1)) by A22, A24, Def2 ;
then reconsider f = chi A,(product (0 ,1 --> INT ,INT )) as Function of (SetVal V,((prop 0 ) => (prop 1))),(SetVal V,(prop 0 )) by A22, CARD_1:88;
A26: 0 in dom (0 .--> p1) by FUNCOP_1:89;
A27: Perm P,(prop 0 ) = P . 0 by Def5
.= (0 .--> p1) . 0 by A26, FUNCT_4:14
.= p1 by FUNCOP_1:87 ;
A28: f is_a_fixpoint_of Perm P,(((prop 0 ) => (prop 1)) => (prop 0 ))

proof

set Q = Perm P,(((prop 0 ) => (prop 1)) => (prop 0 ));
f in Funcs (SetVal V,((prop 0 ) => (prop 1))),(SetVal V,(prop 0 )) by FUNCT_2:11;
then f in SetVal V,(((prop 0 ) => (prop 1)) => (prop 0 )) by Def2;
hence f in dom (Perm P,(((prop 0 ) => (prop 1)) => (prop 0 ))) by FUNCT_2:def 1; :: according to ABIAN:def 3 :: thesis: f = (Perm P,(((prop 0 ) => (prop 1)) => (prop 0 ))) . f
rng ((Perm P,((prop 0 ) => (prop 1))) " ) = dom (((Perm P,((prop 0 ) => (prop 1))) " ) " ) by FUNCT_1:54
.= product (0 ,1 --> INT ,INT ) by A25, FUNCT_2:def 1
.= dom f by FUNCT_2:def 1 ;
then A29: dom (f * ((Perm P,((prop 0 ) => (prop 1))) " )) = dom ((Perm P,((prop 0 ) => (prop 1))) " ) by RELAT_1:46
.= rng (Perm P,((prop 0 ) => (prop 1))) by FUNCT_1:54
.= product (0 ,1 --> INT ,INT ) by A25, FUNCT_2:def 3
.= dom (chi (A ` ),(product (0 ,1 --> INT ,INT ))) by FUNCT_3:def 3 ;
for x being set st x in dom (chi (A ` ),(product (0 ,1 --> INT ,INT ))) holds
(f * ((Perm P,((prop 0 ) => (prop 1))) " )) . x = (chi (A ` ),(product (0 ,1 --> INT ,INT ))) . x

proof

let x be set ; :: thesis: ( x in dom (chi (A ` ),(product (0 ,1 --> INT ,INT ))) implies (f * ((Perm P,((prop 0 ) => (prop 1))) " )) . x = (chi (A ` ),(product (0 ,1 --> INT ,INT ))) . x )
assume A30: x in dom (chi (A ` ),(product (0 ,1 --> INT ,INT ))) ; :: thesis: (f * ((Perm P,((prop 0 ) => (prop 1))) " )) . x = (chi (A ` ),(product (0 ,1 --> INT ,INT ))) . x
then x in product (0 ,1 --> INT ,INT ) by FUNCT_3:def 3;
then x in Funcs (SetVal V,(prop 0 )),(SetVal V,(prop 1)) by A25, Def2;
then reconsider g = x as Function of (SetVal V,(prop 0 )),(SetVal V,(prop 1)) by FUNCT_2:121;
consider i0, j0 being Element of INT such that
A31: g = 0 ,1 --> i0,j0 by A22, A24, Th12;
reconsider i0 = i0, j0 = j0 as Integer ;
A32: not 1 in dom (0 .--> p1) by FUNCOP_1:90;
A33: Perm P,(prop 1) = P . 1 by Def5
.= (NAT --> p0) . 1 by A32, FUNCT_4:12
.= p0 by FUNCOP_1:13 ;
A34: i0 - 1 in dom p0 by A3, INT_1:def 2;
then ex i being Integer st
( i0 - 1 = i & p0 . (i0 - 1) = i + 1 ) by A2, A3;
then p0 . (i0 - 1) = i0 by XCMPLX_1:27;
then A35: (p0 " ) . i0 = i0 - 1 by A34, FUNCT_1:56;
A36: j0 - 1 in dom p0 by A3, INT_1:def 2;
then ex i being Integer st
( j0 - 1 = i & p0 . (j0 - 1) = i + 1 ) by A2, A3;
then A37: p0 . (j0 - 1) = j0 by XCMPLX_1:27;
dom (p0 " ) = INT by A9, FUNCT_1:54;
then A38: ((Perm P,(prop 1)) " ) * g = 0 ,1 --> ((p0 " ) . i0),((p0 " ) . j0) by A31, A33, Th14
.= 0 ,1 --> (i0 - 1),(j0 - 1) by A35, A36, A37, FUNCT_1:56 ;
A39: (f * ((Perm P,((prop 0 ) => (prop 1))) " )) . x = f . (((Perm P,((prop 0 ) => (prop 1))) " ) . x) by A29, A30, FUNCT_1:22
.= f . ((((Perm P,(prop 1)) " ) * g) * (Perm P,(prop 0 ))) by Th38
.= f . (0 ,1 --> (j0 - 1),(i0 - 1)) by A27, A38, Th13 ;

per cases ( x in A or not x in A ) ;

suppose A40: x in A ; :: thesis: (f * ((Perm P,((prop 0 ) => (prop 1))) " )) . x = (chi (A ` ),(product (0 ,1 --> INT ,INT ))) . x

then consider i, j being Element of INT such that
A41: x = 0 ,1 --> i,j and
A42: ( i < j or ( i is even & i = j ) ) ;
A43: ( i = i0 & j = j0 ) by A31, A41, Th10;
A44: x in (A ` ) ` by A40;
( j0 - 1 in INT & i0 - 1 in INT ) by INT_1:def 2;
then A45: 0 ,1 --> (j0 - 1),(i0 - 1) in product (0 ,1 --> INT ,INT ) by Th11;

now

assume 0 ,1 --> (j0 - 1),(i0 - 1) in A ; :: thesis: contradiction
then consider i, j being Element of INT such that
A46: 0 ,1 --> (j0 - 1),(i0 - 1) = 0 ,1 --> i,j and
A47: ( i < j or ( i is even & i = j ) ) ;
A48: ( i = j0 - 1 & j = i0 - 1 ) by A46, Th10;

per cases ( i < j or ( i is even & i = j ) ) by A47;

suppose i < j ; :: thesis: contradiction

hence contradiction by A42, A43, A48, XREAL_1:11; :: thesis: verum

end;

suppose ( i is even & i = j ) ; :: thesis: contradiction

hence contradiction by A42, A43, A48, XCMPLX_1:19; :: thesis: verum

end;

end;

end;

then 0 ,1 --> (j0 - 1),(i0 - 1) in (product (0 ,1 --> INT ,INT )) \ A by A45, XBOOLE_0:def 5;
hence (f * ((Perm P,((prop 0 ) => (prop 1))) " )) . x = 0 by A39, FUNCT_3:43
.= (chi (A ` ),(product (0 ,1 --> INT ,INT ))) . x by A44, FUNCT_3:43 ;
:: thesis: verum

end;

suppose A49: not x in A ; :: thesis: (f * ((Perm P,((prop 0 ) => (prop 1))) " )) . x = (chi (A ` ),(product (0 ,1 --> INT ,INT ))) . x

x in product (0 ,1 --> INT ,INT ) by A31, Th11;
then A50: x in (product (0 ,1 --> INT ,INT )) \ A by A49, XBOOLE_0:def 5;
A51: ( i0 >= j0 & ( not i0 is even or i0 <> j0 ) ) by A31, A49;
A52: ( j0 - 1 is Element of INT & i0 - 1 is Element of INT ) by INT_1:def 2;

now

per cases ( i0 > j0 or ( i0 = j0 & not i0 is even ) ) by A51, XXREAL_0:1;

suppose i0 > j0 ; :: thesis: 0 ,1 --> (j0 - 1),(i0 - 1) in A

then j0 - 1 < i0 - 1 by XREAL_1:11;
hence 0 ,1 --> (j0 - 1),(i0 - 1) in A by A52; :: thesis: verum

end;

suppose ( i0 = j0 & not i0 is even ) ; :: thesis: 0 ,1 --> (j0 - 1),(i0 - 1) in A

hence 0 ,1 --> (j0 - 1),(i0 - 1) in A by A52; :: thesis: verum

end;

end;

end;

hence (f * ((Perm P,((prop 0 ) => (prop 1))) " )) . x = 1 by A39, FUNCT_3:def 3
.= (chi (A ` ),(product (0 ,1 --> INT ,INT ))) . x by A50, FUNCT_3:def 3 ;
:: thesis: verum

end;

end;

end;

then f * ((Perm P,((prop 0 ) => (prop 1))) " ) = chi (A ` ),(product (0 ,1 --> INT ,INT )) by A29, FUNCT_1:9;
hence f = (Perm P,(prop 0 )) * (f * ((Perm P,((prop 0 ) => (prop 1))) " )) by A27, Th9
.= ((Perm P,(prop 0 )) * f) * ((Perm P,((prop 0 ) => (prop 1))) " ) by RELAT_1:55
.= (Perm P,(((prop 0 ) => (prop 1)) => (prop 0 ))) . f by Th37 ;
:: thesis: verum

end;

for x being set holds not x is_a_fixpoint_of Perm P,(prop 0 )

proof

let x be set ; :: thesis: not x is_a_fixpoint_of Perm P,(prop 0 )
assume x in dom (Perm P,(prop 0 )) ; :: according to ABIAN:def 3 :: thesis: not x = (Perm P,(prop 0 )) . x
then x in SetVal V,(prop 0 ) by FUNCT_2:def 1;
then A53: x in V . 0 by Def2;
0 in dom (0 .--> 2) by FUNCOP_1:89;
then V . 0 = (0 .--> 2) . 0 by FUNCT_4:14;
then V . 0 = 2 by FUNCOP_1:87;
then ( x = 0 or x = 1 ) by A53, CARD_1:88, TARSKI:def 2;
hence not x = (Perm P,(prop 0 )) . x by A27, FUNCT_4:66; :: thesis: verum

end;

hence not (((prop 0 ) => (prop 1)) => (prop 0 )) => (prop 0 ) is pseudo-canonical by A28, Th54; :: thesis: verum