let a, b be Element of NAT ; :: thesis: ( a <> b implies not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical )
assume A1: a <> b ; :: thesis: not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical
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 object ; :: 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 Th10; :: 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);
A2: not b in dom (a .--> 2) by A1, FUNCOP_1:75;
reconsider p1 = (0,1) --> (1,0) as Permutation of 2 by Th14;
defpred S₁[ set , set ] means ex i being Integer st
( $1 = i & $2 = i + 1 );
set V = (NAT --> INT) +* (a .--> (Segm 2));
reconsider V = (NAT --> INT) +* (a .--> (Segm 2)) as SetValuation ;
A3: a in dom (a .--> 2) by FUNCOP_1:74;
A4: 2 = (a .--> 2) . a by FUNCOP_1:72
.= V . a by A3, FUNCT_4:13
.= SetVal (V,(prop a)) by Def2 ;
A5: 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
A6: for e being Element of INT holds S₁[e,p0 . e] from FUNCT_2:sch 3(A5);
A7: dom p0 = INT by FUNCT_2:def 1;
for y being object holds
( y in INT iff ex x being object st
( x in dom p0 & y = p0 . x ) )

proof

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

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

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

end;

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

end;

then A10: rng p0 = INT by FUNCT_1:def 3;
A11: p0 is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom p0 or not x2 in dom 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 A12: 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 A6;
hence x1 = x2 by A12, XCMPLX_1:2; :: thesis: verum

end;

A13: SetVal (V,(prop b)) = V . b by Def2
.= (NAT --> INT) . b by A2, FUNCT_4:11
.= INT ;
A14: product ((0,1) --> (INT,INT)) = product (2 --> INT) by CARD_1:50, FUNCT_4:65
.= Funcs (2,INT) by CARD_3:11
.= SetVal (V,((prop a) => (prop b))) by A4, A13, Def2 ;
then reconsider f = chi (A,(product ((0,1) --> (INT,INT)))) as Function of (SetVal (V,((prop a) => (prop b)))),(SetVal (V,(prop a))) by A4, CARD_1:50;
A15: a in dom (a .--> p1) by FUNCOP_1:74;
reconsider p0 = p0 as Permutation of INT by A11, A10, FUNCT_2:57;
set P = (NAT --> p0) +* (a .--> p1);
A16: dom ((NAT --> p0) +* (a .--> p1)) = (dom (NAT --> p0)) \/ (dom (a .--> p1)) by FUNCT_4:def 1
.= (dom (NAT --> p0)) \/ {a}
.= NAT \/ {a}
.= NAT by ZFMISC_1:40 ;
for n being Element of NAT holds ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n)

proof

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

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

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

then n in dom (a .--> 2) by FUNCOP_1:74;
then A18: V . n = (a .--> 2) . a by A17, FUNCT_4:13
.= 2 by FUNCOP_1:72 ;
n in dom (a .--> p1) by A17, FUNCOP_1:74;
then ((NAT --> p0) +* (a .--> p1)) . n = (a .--> p1) . a by A17, FUNCT_4:13
.= p1 by FUNCOP_1:72 ;
hence ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n) by A18; :: thesis: verum

end;

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

then not n in dom (a .--> 2) by FUNCOP_1:75;
then A20: V . n = (NAT --> INT) . n by FUNCT_4:11
.= INT ;
not n in dom (a .--> p1) by A19, FUNCOP_1:75;
then ((NAT --> p0) +* (a .--> p1)) . n = (NAT --> p0) . n by FUNCT_4:11
.= p0 ;
hence ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n) by A20; :: thesis: verum

end;

end;

end;

then reconsider P = (NAT --> p0) +* (a .--> p1) as Permutation of V by A16, Def4;
A21: Perm (P,(prop a)) = P . a by Def5
.= (a .--> p1) . a by A15, FUNCT_4:13
.= p1 by FUNCOP_1:72 ;
A22: f is_a_fixpoint_of Perm (P,(((prop a) => (prop b)) => (prop a)))

proof

set Q = Perm (P,(((prop a) => (prop b)) => (prop a)));
f in Funcs ((SetVal (V,((prop a) => (prop b)))),(SetVal (V,(prop a)))) by FUNCT_2:8;
then f in SetVal (V,(((prop a) => (prop b)) => (prop a))) by Def2;
hence f in dom (Perm (P,(((prop a) => (prop b)) => (prop a)))) by FUNCT_2:def 1; :: according to ABIAN:def 3 :: thesis: f = (Perm (P,(((prop a) => (prop b)) => (prop a)))) . f
rng ((Perm (P,((prop a) => (prop b)))) ") = dom (((Perm (P,((prop a) => (prop b)))) ") ") by FUNCT_1:32
.= product ((0,1) --> (INT,INT)) by A14, FUNCT_2:def 1
.= dom f by FUNCT_2:def 1 ;
then A23: dom (f * ((Perm (P,((prop a) => (prop b)))) ")) = dom ((Perm (P,((prop a) => (prop b)))) ") by RELAT_1:27
.= rng (Perm (P,((prop a) => (prop b)))) by FUNCT_1:32
.= product ((0,1) --> (INT,INT)) by A14, FUNCT_2:def 3
.= dom (chi ((A `),(product ((0,1) --> (INT,INT))))) by FUNCT_3:def 3 ;
for x being object st x in dom (chi ((A `),(product ((0,1) --> (INT,INT))))) holds
(f * ((Perm (P,((prop a) => (prop b)))) ")) . x = (chi ((A `),(product ((0,1) --> (INT,INT))))) . x

proof

A24: dom (p0 ") = INT by A10, FUNCT_1:32;
let x be object ; :: thesis: ( x in dom (chi ((A `),(product ((0,1) --> (INT,INT))))) implies (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = (chi ((A `),(product ((0,1) --> (INT,INT))))) . x )
A25: not b in dom (a .--> p1) by A1, FUNCOP_1:75;
assume A26: x in dom (chi ((A `),(product ((0,1) --> (INT,INT))))) ; :: thesis: (f * ((Perm (P,((prop a) => (prop b)))) ")) . 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 a))),(SetVal (V,(prop b)))) by A14, Def2;
then reconsider g = x as Function of (SetVal (V,(prop a))),(SetVal (V,(prop b))) by FUNCT_2:66;
consider i0, j0 being Element of INT such that
A27: g = (0,1) --> (i0,j0) by A4, A13, Th11;
reconsider i0 = i0, j0 = j0 as Integer ;
A28: j0 - 1 in dom p0 by A7, INT_1:def 2;
then ex i being Integer st
( j0 - 1 = i & p0 . (j0 - 1) = i + 1 ) by A6, A7;
then A29: p0 . (j0 - 1) = j0 by XCMPLX_1:27;
A30: i0 - 1 in dom p0 by A7, INT_1:def 2;
then ex i being Integer st
( i0 - 1 = i & p0 . (i0 - 1) = i + 1 ) by A6, A7;
then p0 . (i0 - 1) = i0 by XCMPLX_1:27;
then A31: (p0 ") . i0 = i0 - 1 by A30, FUNCT_1:34;
Perm (P,(prop b)) = P . b by Def5
.= (NAT --> p0) . b by A25, FUNCT_4:11
.= p0 ;
then A32: ((Perm (P,(prop b))) ") * g = (0,1) --> (((p0 ") . i0),((p0 ") . j0)) by A27, A24, Th13
.= (0,1) --> ((i0 - 1),(j0 - 1)) by A31, A28, A29, FUNCT_1:34 ;
A33: (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = f . (((Perm (P,((prop a) => (prop b)))) ") . x) by A23, A26, FUNCT_1:12
.= f . ((((Perm (P,(prop b))) ") * g) * (Perm (P,(prop a)))) by Th37
.= f . ((0,1) --> ((j0 - 1),(i0 - 1))) by A21, A32, Th12 ;

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

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

then consider i, j being Element of INT such that
A35: x = (0,1) --> (i,j) and
A36: ( i < j or ( i is even & i = j ) ) ;
A37: ( i = i0 & j = j0 ) by A27, A35, Th9;

A38: now :: thesis: not (0,1) --> ((j0 - 1),(i0 - 1)) in A

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

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

suppose i < j ; :: thesis: contradiction

hence contradiction by A36, A37, A41, XREAL_1:9; :: thesis: verum

end;

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

hence contradiction by A36, A37, A41, XCMPLX_1:19; :: thesis: verum

end;

end;

end;

A42: x in (A `) ` by A34;
( 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 Th10;
then (0,1) --> ((j0 - 1),(i0 - 1)) in (product ((0,1) --> (INT,INT))) \ A by A38, XBOOLE_0:def 5;
hence (f * ((Perm (P,((prop a) => (prop b)))) ")) . x = 0 by A33, FUNCT_3:37
.= (chi ((A `),(product ((0,1) --> (INT,INT))))) . x by A42, FUNCT_3:37 ;
:: thesis: verum

end;

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

x in product ((0,1) --> (INT,INT)) by A27, Th10;
then A44: x in (product ((0,1) --> (INT,INT))) \ A by A43, XBOOLE_0:def 5;
A45: j0 - 1 is Element of INT by INT_1:def 2;
A46: ( i0 is odd or i0 <> j0 ) by A27, A43;
A47: i0 - 1 is Element of INT by INT_1:def 2;
A48: i0 >= j0 by A27, A43;

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

per cases ( i0 > j0 or ( i0 = j0 & i0 is odd ) ) by A48, A46, XXREAL_0:1;

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

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

end;

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

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

end;

end;

end;

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

end;

end;

end;

then f * ((Perm (P,((prop a) => (prop b)))) ") = chi ((A `),(product ((0,1) --> (INT,INT)))) by A23;
hence f = (Perm (P,(prop a))) * (f * ((Perm (P,((prop a) => (prop b)))) ")) by A21, Th8
.= ((Perm (P,(prop a))) * f) * ((Perm (P,((prop a) => (prop b)))) ") by RELAT_1:36
.= (Perm (P,(((prop a) => (prop b)) => (prop a)))) . f by Th36 ;
:: thesis: verum

end;

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

proof

let x be set ; :: thesis: not x is_a_fixpoint_of Perm (P,(prop a))
a in dom (a .--> 2) by FUNCOP_1:74;
then V . a = (a .--> 2) . a by FUNCT_4:13;
then A49: V . a = 2 by FUNCOP_1:72;
assume x in dom (Perm (P,(prop a))) ; :: according to ABIAN:def 3 :: thesis: not x = (Perm (P,(prop a))) . x
then x in SetVal (V,(prop a)) by FUNCT_2:def 1;
then x in V . a by Def2;
then ( x = 0 or x = 1 ) by A49, CARD_1:50, TARSKI:def 2;
hence not x = (Perm (P,(prop a))) . x by A21, FUNCT_4:63; :: thesis: verum

end;

hence not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical by A22, Th43; :: thesis: verum