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))

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_{1}[ 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_{1}[e,u]

A6: for e being Element of INT holds S_{1}[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 ) )

A11: p0 is one-to-one

.= (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)

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)))

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

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))) ;
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;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

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

( $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

proof

consider p0 being Function of INT,INT such that
let e be Element of INT ; :: thesis: ex u being Element of INT st S_{1}[e,u]

reconsider e = e as Integer ;

reconsider u = e + 1 as Element of INT by INT_1:def 2;

take u ; :: thesis: S_{1}[e,u]

thus S_{1}[e,u]
; :: thesis: verum

end;reconsider e = e as Integer ;

reconsider u = e + 1 as Element of INT by INT_1:def 2;

take u ; :: thesis: S

thus S

A6: for e being Element of INT holds S

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

then A10:
rng p0 = INT
by FUNCT_1:def 3;
let y be object ; :: thesis: ( y in INT iff ex x being object st

( x in dom p0 & y = p0 . x ) )

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;( 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 )

given x being object such that A8:
x in dom p0
and ( 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;( 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

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

A11: p0 is one-to-one

proof

A13: SetVal (V,(prop b)) =
V . b
by Def2
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;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

.= (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

then reconsider P = (NAT --> p0) +* (a .--> p1) as Permutation of V by A16, Def4;
let n be Element of NAT ; :: thesis: ((NAT --> p0) +* (a .--> p1)) . n is Permutation of (V . n)

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

end;

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;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

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;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

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

for x being set holds not x is_a_fixpoint_of Perm (P,(prop a))
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

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;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

then
f * ((Perm (P,((prop a) => (prop b)))) ") = chi ((A `),(product ((0,1) --> (INT,INT))))
by A23;
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 ;

end;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 )
;

end;

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;

( 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;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

A42:
x in (A `) `
by A34;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;

end;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;

( 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

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;

.= (chi ((A `),(product ((0,1) --> (INT,INT))))) . x by A44, FUNCT_3:def 3 ;

:: thesis: verum

end;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

hence (f * ((Perm (P,((prop a) => (prop b)))) ")) . x =
1
by A33, FUNCT_3:def 3
end;

.= (chi ((A `),(product ((0,1) --> (INT,INT))))) . x by A44, FUNCT_3:def 3 ;

:: thesis: verum

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

proof

hence
not (((prop a) => (prop b)) => (prop a)) => (prop a) is pseudo-canonical
by A22, Th43; :: thesis: verum
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;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