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 ex i, j being Element of INT st
( x = (0,1) --> (i,j) & ( i < j or ( i is even & i = j ) ) ) ;
hence x in product ((0,1) --> (INT,INT)) by 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))) ;
set p1 = (0,1) --> (1,0);
A1: not 1 in dom (0 .--> 2) by FUNCOP_1:90;
A2: dom ((0,1) --> (1,0)) = 2 by CARD_1:88, FUNCT_4:65;
A3: (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 that
A4: x1 in dom ((0,1) --> (1,0)) and
A5: x2 in dom ((0,1) --> (1,0)) ; :: thesis: ( not ((0,1) --> (1,0)) . x1 = ((0,1) --> (1,0)) . x2 or x1 = x2 )
A6: ( x2 = 0 or x2 = 1 ) by A2, A5, CARD_1:88, TARSKI:def 2;
A7: ((0,1) --> (1,0)) . 0 = 1 by FUNCT_4:66;
( x1 = 0 or x1 = 1 ) by A2, A4, CARD_1:88, TARSKI:def 2;
hence ( not ((0,1) --> (1,0)) . x1 = ((0,1) --> (1,0)) . x2 or x1 = x2 ) by A6, A7, FUNCT_4:66; :: thesis: verum

end;

A8: rng ((0,1) --> (1,0)) = 2 by CARD_1:88, FUNCT_4:67;
then (0,1) --> (1,0) is Function of 2,2 by A2, FUNCT_2:def 1, RELSET_1:11;
then reconsider p1 = (0,1) --> (1,0) as Permutation of 2 by A8, A3, FUNCT_2:83;
defpred S₁[ set , set ] means ex i being Integer st
( $1 = i & $2 = i + 1 );
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 NAT by PARTFUN1:def 4;
reconsider V = V as SetValuation ;
A9: 0 in dom (0 .--> 2) by FUNCOP_1:89;
A10: 2 = (0 .--> 2) . 0 by FUNCOP_1:87
.= V . 0 by A9, FUNCT_4:14
.= SetVal (V,(prop 0)) by Def2 ;
A11: 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
A12: for e being Element of INT holds S₁[e,p0 . e] from FUNCT_2:sch 3(A11);
A13: dom p0 = INT by FUNCT_2:def 1;
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 A13, INT_1:def 2; :: thesis: y = p0 . x
then ex j being Integer st
( x = j & p0 . x = j + 1 ) by A12, A13;
hence y = p0 . x by XCMPLX_1:27; :: thesis: verum

end;

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

end;

then A16: rng p0 = INT by FUNCT_1:def 5;
A17: 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;
assume A18: p0 . x1 = p0 . x2 ; :: thesis: x1 = x2
( ex i1 being Integer st
( I1 = i1 & p0 . I1 = i1 + 1 ) & ex i2 being Integer st
( I2 = i2 & p0 . I2 = i2 + 1 ) ) by A12;
hence x1 = x2 by A18, XCMPLX_1:2; :: thesis: verum

end;

A19: SetVal (V,(prop 1)) = V . 1 by Def2
.= (NAT --> INT) . 1 by A1, FUNCT_4:12
.= INT by FUNCOP_1:13 ;
A20: 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 A10, A19, 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 A10, CARD_1:88;
A21: 0 in dom (0 .--> p1) by FUNCOP_1:89;
reconsider p0 = p0 as Permutation of INT by A17, A16, FUNCT_2:83;
set P = (NAT --> p0) +* (0 .--> p1);
A22: 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 A23: n = 0 ; :: thesis: ((NAT --> p0) +* (0 .--> p1)) . n is Permutation of (V . n)

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

end;

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

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

end;

end;

end;

then reconsider P = (NAT --> p0) +* (0 .--> p1) as Permutation of V by A22, Def4;
A27: Perm (P,(prop 0)) = P . 0 by Def5
.= (0 .--> p1) . 0 by A21, 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 A20, 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 A20, 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

A30: dom (p0 ") = INT by A16, FUNCT_1:54;
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 )
A31: not 1 in dom (0 .--> p1) by FUNCOP_1:90;
assume A32: 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 A20, 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
A33: g = (0,1) --> (i0,j0) by A10, A19, Th12;
reconsider i0 = i0, j0 = j0 as Integer ;
A34: j0 - 1 in dom p0 by A13, INT_1:def 2;
then ex i being Integer st
( j0 - 1 = i & p0 . (j0 - 1) = i + 1 ) by A12, A13;
then A35: p0 . (j0 - 1) = j0 by XCMPLX_1:27;
A36: i0 - 1 in dom p0 by A13, INT_1:def 2;
then ex i being Integer st
( i0 - 1 = i & p0 . (i0 - 1) = i + 1 ) by A12, A13;
then p0 . (i0 - 1) = i0 by XCMPLX_1:27;
then A37: (p0 ") . i0 = i0 - 1 by A36, FUNCT_1:56;
Perm (P,(prop 1)) = P . 1 by Def5
.= (NAT --> p0) . 1 by A31, FUNCT_4:12
.= p0 by FUNCOP_1:13 ;
then A38: ((Perm (P,(prop 1))) ") * g = (0,1) --> (((p0 ") . i0),((p0 ") . j0)) by A33, A30, Th14
.= (0,1) --> ((i0 - 1),(j0 - 1)) by A37, A34, A35, FUNCT_1:56 ;
A39: (f * ((Perm (P,((prop 0) => (prop 1)))) ")) . x = f . (((Perm (P,((prop 0) => (prop 1)))) ") . x) by A29, A32, 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 A33, A41, Th10;

A44: now

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

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

suppose i < j ; :: thesis: contradiction

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

end;

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

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

end;

end;

end;

A48: x in (A `) ` by A40;
( j0 - 1 in INT & i0 - 1 in INT ) by INT_1:def 2;
then (0,1) --> ((j0 - 1),(i0 - 1)) in product ((0,1) --> (INT,INT)) by Th11;
then (0,1) --> ((j0 - 1),(i0 - 1)) in (product ((0,1) --> (INT,INT))) \ A by A44, 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 A48, 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 A33, Th11;
then A50: x in (product ((0,1) --> (INT,INT))) \ A by A49, XBOOLE_0:def 5;
A51: j0 - 1 is Element of INT by INT_1:def 2;
A52: ( not i0 is even or i0 <> j0 ) by A33, A49;
A53: i0 - 1 is Element of INT by INT_1:def 2;
A54: i0 >= j0 by A33, A49;

now

per cases ( i0 > j0 or ( i0 = j0 & not i0 is even ) ) by A54, A52, 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 A51, A53; :: 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 A51; :: 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))
0 in dom (0 .--> 2) by FUNCOP_1:89;
then V . 0 = (0 .--> 2) . 0 by FUNCT_4:14;
then A55: V . 0 = 2 by FUNCOP_1:87;
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 x in V . 0 by Def2;
then ( x = 0 or x = 1 ) by A55, 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