let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)

for p being Element of CQC-WFF Al holds

( X |- 'not' p iff X \/ {p} is Inconsistent )

let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al holds

( X |- 'not' p iff X \/ {p} is Inconsistent )

let p be Element of CQC-WFF Al; :: thesis: ( X |- 'not' p iff X \/ {p} is Inconsistent )

thus ( X |- 'not' p implies X \/ {p} is Inconsistent ) :: thesis: ( X \/ {p} is Inconsistent implies X |- 'not' p )

for p being Element of CQC-WFF Al holds

( X |- 'not' p iff X \/ {p} is Inconsistent )

let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al holds

( X |- 'not' p iff X \/ {p} is Inconsistent )

let p be Element of CQC-WFF Al; :: thesis: ( X |- 'not' p iff X \/ {p} is Inconsistent )

thus ( X |- 'not' p implies X \/ {p} is Inconsistent ) :: thesis: ( X \/ {p} is Inconsistent implies X |- 'not' p )

proof

thus
( X \/ {p} is Inconsistent implies X |- 'not' p )
:: thesis: verum
assume
X |- 'not' p
; :: thesis: X \/ {p} is Inconsistent

then consider f being FinSequence of CQC-WFF Al such that

A1: rng f c= X and

A2: |- f ^ <*('not' p)*> ;

set f2 = f ^ <*p*>;

set f1 = (f ^ <*p*>) ^ <*p*>;

A3: Ant ((f ^ <*p*>) ^ <*p*>) = f ^ <*p*> by CALCUL_1:5;

1 in Seg 1 by FINSEQ_1:1;

then 1 in dom <*p*> by FINSEQ_1:38;

then A4: (len f) + 1 in dom (Ant ((f ^ <*p*>) ^ <*p*>)) by A3, FINSEQ_1:28;

Suc ((f ^ <*p*>) ^ <*p*>) = p by CALCUL_1:5;

then (Ant ((f ^ <*p*>) ^ <*p*>)) . ((len f) + 1) = Suc ((f ^ <*p*>) ^ <*p*>) by A3, FINSEQ_1:42;

then Suc ((f ^ <*p*>) ^ <*p*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p*>) by A4, CALCUL_1:def 16;

then A5: |- (f ^ <*p*>) ^ <*p*> by CALCUL_1:33;

A6: 0 + 1 <= len (f ^ <*p*>) by CALCUL_1:10;

( Ant (f ^ <*p*>) = f & Suc (f ^ <*p*>) = p ) by CALCUL_1:5;

then A7: rng (f ^ <*p*>) = (rng f) \/ {p} by A6, CALCUL_1:3;

|- (f ^ <*p*>) ^ <*('not' p)*> by A2, Th5;

then not f ^ <*p*> is Consistent by A5;

hence X \/ {p} is Inconsistent by A1, A7, Th4, XBOOLE_1:9; :: thesis: verum

end;then consider f being FinSequence of CQC-WFF Al such that

A1: rng f c= X and

A2: |- f ^ <*('not' p)*> ;

set f2 = f ^ <*p*>;

set f1 = (f ^ <*p*>) ^ <*p*>;

A3: Ant ((f ^ <*p*>) ^ <*p*>) = f ^ <*p*> by CALCUL_1:5;

1 in Seg 1 by FINSEQ_1:1;

then 1 in dom <*p*> by FINSEQ_1:38;

then A4: (len f) + 1 in dom (Ant ((f ^ <*p*>) ^ <*p*>)) by A3, FINSEQ_1:28;

Suc ((f ^ <*p*>) ^ <*p*>) = p by CALCUL_1:5;

then (Ant ((f ^ <*p*>) ^ <*p*>)) . ((len f) + 1) = Suc ((f ^ <*p*>) ^ <*p*>) by A3, FINSEQ_1:42;

then Suc ((f ^ <*p*>) ^ <*p*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p*>) by A4, CALCUL_1:def 16;

then A5: |- (f ^ <*p*>) ^ <*p*> by CALCUL_1:33;

A6: 0 + 1 <= len (f ^ <*p*>) by CALCUL_1:10;

( Ant (f ^ <*p*>) = f & Suc (f ^ <*p*>) = p ) by CALCUL_1:5;

then A7: rng (f ^ <*p*>) = (rng f) \/ {p} by A6, CALCUL_1:3;

|- (f ^ <*p*>) ^ <*('not' p)*> by A2, Th5;

then not f ^ <*p*> is Consistent by A5;

hence X \/ {p} is Inconsistent by A1, A7, Th4, XBOOLE_1:9; :: thesis: verum

proof

assume
X \/ {p} is Inconsistent
; :: thesis: X |- 'not' p

then X \/ {p} |- 'not' p by Th6;

then consider f being FinSequence of CQC-WFF Al such that

A8: rng f c= X \/ {p} and

A9: |- f ^ <*('not' p)*> ;

end;then X \/ {p} |- 'not' p by Th6;

then consider f being FinSequence of CQC-WFF Al such that

A8: rng f c= X \/ {p} and

A9: |- f ^ <*('not' p)*> ;

now :: thesis: ( not rng f c= X implies X |- 'not' p )

hence
X |- 'not' p
by A9; :: thesis: verumset g = f - {p};

reconsider A = f " {p} as finite set ;

reconsider B = dom f as finite set ;

set n = card A;

set h = (f - {p}) ^ (IdFinS (p,(card A)));

A10: len (IdFinS (p,(card A))) = card A by CARD_1:def 7;

A c= B by RELAT_1:132;

then A11: A c= Seg (len f) by FINSEQ_1:def 3;

then consider a being object such that

A17: a in rng f and

A18: not a in X ;

( a in X or a in {p} ) by A8, A17, XBOOLE_0:def 3;

then a = p by A18, TARSKI:def 1;

then consider i being Nat such that

A19: i in B and

A20: f . i = p by A17, FINSEQ_2:10;

reconsider C = B \ A as finite set ;

defpred S_{1}[ Nat, object ] means ( ( $1 in Seg (len (f - {p})) implies $2 = (Sgm (B \ A)) . $1 ) & ( $1 in seq ((len (f - {p})),(card A)) implies $2 = (Sgm A) . ($1 - (len (f - {p}))) ) );

A21: card C = (card B) - (card A) by CARD_2:44, RELAT_1:132

.= (card (Seg (len f))) - (card A) by FINSEQ_1:def 3

.= (len f) - (card A) by FINSEQ_1:57

.= len (f - {p}) by FINSEQ_3:59 ;

A22: for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) holds

ex a being object st S_{1}[k,a]

A24: ( dom F = Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) & ( for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) holds

S_{1}[k,F . k] ) )
from FINSEQ_1:sch 1(A22);

then A26: dom (Sgm C) = Seg (card C) by FINSEQ_3:40;

A27: rng F = B

.= ((len f) - (card A)) + (len (IdFinS (p,(card A)))) by FINSEQ_3:59

.= ((len f) - (card A)) + (card A) by CARD_1:def 7

.= len f ;

then A52: dom F = B by A24, FINSEQ_1:def 3;

then reconsider F = F as Relation of B,B by A27, RELSET_1:4;

rng F c= B ;

then reconsider F = F as Function of B,B by A52, FUNCT_2:2;

F is one-to-one

consider j being Nat such that

A74: j in dom F and

A75: F . j = i by A27, A19, FINSEQ_2:10;

A76: dom (Per (f,F)) = B by CALCUL_2:19

.= dom F by A24, A51, FINSEQ_1:def 3

.= dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A24, FINSEQ_1:def 3 ;

reconsider h = (f - {p}) ^ (IdFinS (p,(card A))) as FinSequence of CQC-WFF Al by A76, A77, FINSEQ_1:13;

(F * f) . j = p by A20, A74, A75, FUNCT_1:13;

then A93: h . j = p by A92, CALCUL_2:def 2;

then j in dom h by A76, CALCUL_2:19;

then consider k being Nat such that

A98: k in dom (IdFinS (p,(card A))) and

j = (len (f - {p})) + k by A94, FINSEQ_1:25;

reconsider g = f - {p} as FinSequence of CQC-WFF Al by FINSEQ_3:86;

( 1 <= k & k <= len (IdFinS (p,(card A))) ) by A98, FINSEQ_3:25;

then 1 <= len (IdFinS (p,(card A))) by XXREAL_0:2;

then A99: 1 <= card A by CARD_1:def 7;

|- h ^ <*('not' p)*> by A9, A92, CALCUL_2:30;

then A100: |- (g ^ <*p*>) ^ <*('not' p)*> by A99, CALCUL_2:32;

( rng g = (rng f) \ {p} & (rng f) \ {p} c= (X \/ {p}) \ {p} ) by A8, FINSEQ_3:65, XBOOLE_1:33;

then A101: rng g c= X \ {p} by XBOOLE_1:40;

X \ {p} c= X by XBOOLE_1:36;

then A102: rng g c= X by A101;

|- (g ^ <*('not' p)*>) ^ <*('not' p)*> by CALCUL_2:21;

then |- g ^ <*('not' p)*> by A100, CALCUL_2:26;

hence X |- 'not' p by A102; :: thesis: verum

end;reconsider A = f " {p} as finite set ;

reconsider B = dom f as finite set ;

set n = card A;

set h = (f - {p}) ^ (IdFinS (p,(card A)));

A10: len (IdFinS (p,(card A))) = card A by CARD_1:def 7;

A c= B by RELAT_1:132;

then A11: A c= Seg (len f) by FINSEQ_1:def 3;

A12: now :: thesis: for i being Nat st i in seq ((len (f - {p})),(card A)) holds

i - (len (f - {p})) in dom (Sgm A)

assume
not rng f c= X
; :: thesis: X |- 'not' pi - (len (f - {p})) in dom (Sgm A)

let i be Nat; :: thesis: ( i in seq ((len (f - {p})),(card A)) implies i - (len (f - {p})) in dom (Sgm A) )

reconsider j = i - (len (f - {p})) as Integer ;

assume A13: i in seq ((len (f - {p})),(card A)) ; :: thesis: i - (len (f - {p})) in dom (Sgm A)

then A14: 1 + (len (f - {p})) <= i by CALCUL_2:1;

then A15: 1 <= j by XREAL_1:19;

i <= (card A) + (len (f - {p})) by A13, CALCUL_2:1;

then A16: j <= card A by XREAL_1:20;

0 <= j by A14, XREAL_1:19;

then reconsider j = j as Element of NAT by INT_1:3;

j in Seg (card A) by A15, A16, FINSEQ_1:1;

hence i - (len (f - {p})) in dom (Sgm A) by A11, FINSEQ_3:40; :: thesis: verum

end;reconsider j = i - (len (f - {p})) as Integer ;

assume A13: i in seq ((len (f - {p})),(card A)) ; :: thesis: i - (len (f - {p})) in dom (Sgm A)

then A14: 1 + (len (f - {p})) <= i by CALCUL_2:1;

then A15: 1 <= j by XREAL_1:19;

i <= (card A) + (len (f - {p})) by A13, CALCUL_2:1;

then A16: j <= card A by XREAL_1:20;

0 <= j by A14, XREAL_1:19;

then reconsider j = j as Element of NAT by INT_1:3;

j in Seg (card A) by A15, A16, FINSEQ_1:1;

hence i - (len (f - {p})) in dom (Sgm A) by A11, FINSEQ_3:40; :: thesis: verum

then consider a being object such that

A17: a in rng f and

A18: not a in X ;

( a in X or a in {p} ) by A8, A17, XBOOLE_0:def 3;

then a = p by A18, TARSKI:def 1;

then consider i being Nat such that

A19: i in B and

A20: f . i = p by A17, FINSEQ_2:10;

reconsider C = B \ A as finite set ;

defpred S

A21: card C = (card B) - (card A) by CARD_2:44, RELAT_1:132

.= (card (Seg (len f))) - (card A) by FINSEQ_1:def 3

.= (len f) - (card A) by FINSEQ_1:57

.= len (f - {p}) by FINSEQ_3:59 ;

A22: for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) holds

ex a being object st S

proof

consider F being FinSequence such that
let k be Nat; :: thesis: ( k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) implies ex a being object st S_{1}[k,a] )

assume k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) ; :: thesis: ex a being object st S_{1}[k,a]

_{1}[k,a]
; :: thesis: verum

end;assume k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) ; :: thesis: ex a being object st S

now :: thesis: ( k in Seg (len (f - {p})) implies ex a being set st S_{1}[k,a] )

hence
ex a being object st Sassume A23:
k in Seg (len (f - {p}))
; :: thesis: ex a being set st S_{1}[k,a]

take a = (Sgm (B \ A)) . k; :: thesis: S_{1}[k,a]

Seg (len (f - {p})) misses seq ((len (f - {p})),(card A)) by CALCUL_2:8;

hence S_{1}[k,a]
by A23, XBOOLE_0:3; :: thesis: verum

end;take a = (Sgm (B \ A)) . k; :: thesis: S

Seg (len (f - {p})) misses seq ((len (f - {p})),(card A)) by CALCUL_2:8;

hence S

A24: ( dom F = Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) & ( for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) holds

S

now :: thesis: for b being object st b in C holds

b in Seg (len f)

then A25:
C c= Seg (len f)
;b in Seg (len f)

let b be object ; :: thesis: ( b in C implies b in Seg (len f) )

assume b in C ; :: thesis: b in Seg (len f)

then b in dom f ;

hence b in Seg (len f) by FINSEQ_1:def 3; :: thesis: verum

end;assume b in C ; :: thesis: b in Seg (len f)

then b in dom f ;

hence b in Seg (len f) by FINSEQ_1:def 3; :: thesis: verum

then A26: dom (Sgm C) = Seg (card C) by FINSEQ_3:40;

A27: rng F = B

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in rng F )

assume A35: a in B ; :: thesis: a in rng F

end;

A51: len ((f - {p}) ^ (IdFinS (p,(card A)))) =
(len (f - {p})) + (len (IdFinS (p,(card A))))
by FINSEQ_1:22
now :: thesis: for a being object st a in rng F holds

a in B

hence
rng F c= B
; :: according to XBOOLE_0:def 10 :: thesis: B c= rng Fa in B

let a be object ; :: thesis: ( a in rng F implies a in B )

assume a in rng F ; :: thesis: a in B

then consider i being Nat such that

A28: i in dom F and

A29: F . i = a by FINSEQ_2:10;

hence a in B by A30, A31, XBOOLE_0:def 3; :: thesis: verum

end;assume a in rng F ; :: thesis: a in B

then consider i being Nat such that

A28: i in dom F and

A29: F . i = a by FINSEQ_2:10;

A30: now :: thesis: ( i in Seg (len (f - {p})) implies a in B )

assume
i in Seg (len (f - {p}))
; :: thesis: a in B

then ( a = (Sgm C) . i & i in dom (Sgm C) ) by A24, A25, A21, A28, A29, FINSEQ_3:40;

then a in rng (Sgm C) by FUNCT_1:3;

then a in C by A25, FINSEQ_1:def 13;

hence a in B ; :: thesis: verum

end;then ( a = (Sgm C) . i & i in dom (Sgm C) ) by A24, A25, A21, A28, A29, FINSEQ_3:40;

then a in rng (Sgm C) by FUNCT_1:3;

then a in C by A25, FINSEQ_1:def 13;

hence a in B ; :: thesis: verum

A31: now :: thesis: ( i in seq ((len (f - {p})),(card A)) implies a in B )

i in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A)))
by A10, A24, A28, Lm1;A32:
rng (Sgm A) = A
by A11, FINSEQ_1:def 13;

A33: A c= B by RELAT_1:132;

assume A34: i in seq ((len (f - {p})),(card A)) ; :: thesis: a in B

then a = (Sgm A) . (i - (len (f - {p}))) by A24, A28, A29;

then a in A by A12, A34, A32, FUNCT_1:3;

hence a in B by A33; :: thesis: verum

end;A33: A c= B by RELAT_1:132;

assume A34: i in seq ((len (f - {p})),(card A)) ; :: thesis: a in B

then a = (Sgm A) . (i - (len (f - {p}))) by A24, A28, A29;

then a in A by A12, A34, A32, FUNCT_1:3;

hence a in B by A33; :: thesis: verum

hence a in B by A30, A31, XBOOLE_0:def 3; :: thesis: verum

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in rng F )

assume A35: a in B ; :: thesis: a in rng F

A36: now :: thesis: ( not a in A implies a in rng F )

assume not a in A ; :: thesis: a in rng F

then a in C by A35, XBOOLE_0:def 5;

then a in rng (Sgm C) by A37, FINSEQ_1:def 13;

then consider i being Nat such that

A38: i in dom (Sgm C) and

A39: (Sgm C) . i = a by FINSEQ_2:10;

A40: 1 <= i by A38, FINSEQ_3:25;

len (Sgm C) = len (f - {p}) by A26, A21, FINSEQ_1:def 3;

then A41: i <= len (f - {p}) by A38, FINSEQ_3:25;

len (f - {p}) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by CALCUL_1:6;

then i <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by A41, XXREAL_0:2;

then A42: i in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A40, FINSEQ_1:1;

i in Seg (len (f - {p})) by A40, A41, FINSEQ_1:1;

then a = F . i by A24, A39, A42;

hence a in rng F by A24, A42, FUNCT_1:3; :: thesis: verum

end;

now :: thesis: for b being object st b in C holds

b in Seg (len f)

then A37:
C c= Seg (len f)
;b in Seg (len f)

let b be object ; :: thesis: ( b in C implies b in Seg (len f) )

assume b in C ; :: thesis: b in Seg (len f)

then b in dom f ;

hence b in Seg (len f) by FINSEQ_1:def 3; :: thesis: verum

end;assume b in C ; :: thesis: b in Seg (len f)

then b in dom f ;

hence b in Seg (len f) by FINSEQ_1:def 3; :: thesis: verum

assume not a in A ; :: thesis: a in rng F

then a in C by A35, XBOOLE_0:def 5;

then a in rng (Sgm C) by A37, FINSEQ_1:def 13;

then consider i being Nat such that

A38: i in dom (Sgm C) and

A39: (Sgm C) . i = a by FINSEQ_2:10;

A40: 1 <= i by A38, FINSEQ_3:25;

len (Sgm C) = len (f - {p}) by A26, A21, FINSEQ_1:def 3;

then A41: i <= len (f - {p}) by A38, FINSEQ_3:25;

len (f - {p}) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by CALCUL_1:6;

then i <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by A41, XXREAL_0:2;

then A42: i in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A40, FINSEQ_1:1;

i in Seg (len (f - {p})) by A40, A41, FINSEQ_1:1;

then a = F . i by A24, A39, A42;

hence a in rng F by A24, A42, FUNCT_1:3; :: thesis: verum

now :: thesis: ( a in A implies a in rng F )

hence
a in rng F
by A36; :: thesis: verumassume A43:
a in A
; :: thesis: a in rng F

rng (Sgm A) = A by A11, FINSEQ_1:def 13;

then consider i being Nat such that

A44: i in dom (Sgm A) and

A45: (Sgm A) . i = a by A43, FINSEQ_2:10;

reconsider i = i as Nat ;

set m = i + (len (f - {p}));

len (Sgm A) = card A by A11, FINSEQ_3:39;

then i <= card A by A44, FINSEQ_3:25;

then A46: i + (len (f - {p})) <= (card A) + (len (f - {p})) by XREAL_1:6;

then i + (len (f - {p})) <= (len (f - {p})) + (len (IdFinS (p,(card A)))) by CARD_1:def 7;

then A47: i + (len (f - {p})) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by FINSEQ_1:22;

A48: 1 <= i by A44, FINSEQ_3:25;

then 1 + (len (f - {p})) <= i + (len (f - {p})) by XREAL_1:6;

then A49: i + (len (f - {p})) in seq ((len (f - {p})),(card A)) by A46, CALCUL_2:1;

i <= i + (len (f - {p})) by NAT_1:11;

then 1 <= i + (len (f - {p})) by A48, XXREAL_0:2;

then i + (len (f - {p})) in dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A47, FINSEQ_3:25;

then A50: i + (len (f - {p})) in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by FINSEQ_1:def 3;

a = (Sgm A) . ((i + (len (f - {p}))) - (len (f - {p}))) by A45;

then a = F . (i + (len (f - {p}))) by A24, A49, A50;

hence a in rng F by A24, A50, FUNCT_1:3; :: thesis: verum

end;rng (Sgm A) = A by A11, FINSEQ_1:def 13;

then consider i being Nat such that

A44: i in dom (Sgm A) and

A45: (Sgm A) . i = a by A43, FINSEQ_2:10;

reconsider i = i as Nat ;

set m = i + (len (f - {p}));

len (Sgm A) = card A by A11, FINSEQ_3:39;

then i <= card A by A44, FINSEQ_3:25;

then A46: i + (len (f - {p})) <= (card A) + (len (f - {p})) by XREAL_1:6;

then i + (len (f - {p})) <= (len (f - {p})) + (len (IdFinS (p,(card A)))) by CARD_1:def 7;

then A47: i + (len (f - {p})) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by FINSEQ_1:22;

A48: 1 <= i by A44, FINSEQ_3:25;

then 1 + (len (f - {p})) <= i + (len (f - {p})) by XREAL_1:6;

then A49: i + (len (f - {p})) in seq ((len (f - {p})),(card A)) by A46, CALCUL_2:1;

i <= i + (len (f - {p})) by NAT_1:11;

then 1 <= i + (len (f - {p})) by A48, XXREAL_0:2;

then i + (len (f - {p})) in dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A47, FINSEQ_3:25;

then A50: i + (len (f - {p})) in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by FINSEQ_1:def 3;

a = (Sgm A) . ((i + (len (f - {p}))) - (len (f - {p}))) by A45;

then a = F . (i + (len (f - {p}))) by A24, A49, A50;

hence a in rng F by A24, A50, FUNCT_1:3; :: thesis: verum

.= ((len f) - (card A)) + (len (IdFinS (p,(card A)))) by FINSEQ_3:59

.= ((len f) - (card A)) + (card A) by CARD_1:def 7

.= len f ;

then A52: dom F = B by A24, FINSEQ_1:def 3;

then reconsider F = F as Relation of B,B by A27, RELSET_1:4;

rng F c= B ;

then reconsider F = F as Function of B,B by A52, FUNCT_2:2;

F is one-to-one

proof

then reconsider F = F as Permutation of (dom f) by A27, FUNCT_2:57;
let a1, a2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a1 in dom F or not a2 in dom F or not F . a1 = F . a2 or a1 = a2 )

assume that

A53: a1 in dom F and

A54: a2 in dom F and

A55: F . a1 = F . a2 ; :: thesis: a1 = a2

A56: a2 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A10, A24, A54, Lm1;

hence a1 = a2 by A57, A66, XBOOLE_0:def 3; :: thesis: verum

end;assume that

A53: a1 in dom F and

A54: a2 in dom F and

A55: F . a1 = F . a2 ; :: thesis: a1 = a2

A56: a2 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A10, A24, A54, Lm1;

A57: now :: thesis: ( a1 in Seg (len (f - {p})) implies a1 = a2 )

assume A58:
a1 in Seg (len (f - {p}))
; :: thesis: a1 = a2

then A59: a1 in dom (Sgm C) by A25, A21, FINSEQ_3:40;

F . a1 = (Sgm C) . a1 by A24, A53, A58;

then F . a1 in rng (Sgm C) by A59, FUNCT_1:3;

then A60: F . a1 in C by A25, FINSEQ_1:def 13;

end;then A59: a1 in dom (Sgm C) by A25, A21, FINSEQ_3:40;

F . a1 = (Sgm C) . a1 by A24, A53, A58;

then F . a1 in rng (Sgm C) by A59, FUNCT_1:3;

then A60: F . a1 in C by A25, FINSEQ_1:def 13;

A61: now :: thesis: not a2 in seq ((len (f - {p})),(card A))

assume A62:
a2 in seq ((len (f - {p})),(card A))
; :: thesis: contradiction

then reconsider i = a2 as Nat ;

(Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A12, A62, FUNCT_1:3;

then F . a2 in rng (Sgm A) by A24, A54, A62;

then F . a2 in A by A11, FINSEQ_1:def 13;

hence contradiction by A55, A60, XBOOLE_0:def 5; :: thesis: verum

end;then reconsider i = a2 as Nat ;

(Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A12, A62, FUNCT_1:3;

then F . a2 in rng (Sgm A) by A24, A54, A62;

then F . a2 in A by A11, FINSEQ_1:def 13;

hence contradiction by A55, A60, XBOOLE_0:def 5; :: thesis: verum

now :: thesis: ( a2 in Seg (len (f - {p})) implies a1 = a2 )

hence
a1 = a2
by A56, A61, XBOOLE_0:def 3; :: thesis: verumassume A63:
a2 in Seg (len (f - {p}))
; :: thesis: a1 = a2

then F . a2 = (Sgm C) . a2 by A24, A54;

then A64: (Sgm C) . a1 = (Sgm C) . a2 by A24, A53, A55, A58;

A65: Sgm C is one-to-one by A25, FINSEQ_3:92;

a2 in dom (Sgm C) by A25, A21, A63, FINSEQ_3:40;

hence a1 = a2 by A59, A64, A65; :: thesis: verum

end;then F . a2 = (Sgm C) . a2 by A24, A54;

then A64: (Sgm C) . a1 = (Sgm C) . a2 by A24, A53, A55, A58;

A65: Sgm C is one-to-one by A25, FINSEQ_3:92;

a2 in dom (Sgm C) by A25, A21, A63, FINSEQ_3:40;

hence a1 = a2 by A59, A64, A65; :: thesis: verum

A66: now :: thesis: ( a1 in seq ((len (f - {p})),(card A)) implies a1 = a2 )

a1 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A)))
by A10, A24, A53, Lm1;assume A67:
a1 in seq ((len (f - {p})),(card A))
; :: thesis: a1 = a2

then reconsider i = a1 as Nat ;

A68: i - (len (f - {p})) in dom (Sgm A) by A12, A67;

then F . a1 in rng (Sgm A) by A24, A53, A67;

then A73: F . a1 in A by A11, FINSEQ_1:def 13;

end;then reconsider i = a1 as Nat ;

A68: i - (len (f - {p})) in dom (Sgm A) by A12, A67;

A69: now :: thesis: ( a2 in seq ((len (f - {p})),(card A)) implies a1 = a2 )

(Sgm A) . (i - (len (f - {p}))) in rng (Sgm A)
by A12, A67, FUNCT_1:3;assume A70:
a2 in seq ((len (f - {p})),(card A))
; :: thesis: a1 = a2

then reconsider i1 = a2 as Nat ;

F . a2 = (Sgm A) . (i1 - (len (f - {p}))) by A24, A54, A70;

then A71: (Sgm A) . (i1 - (len (f - {p}))) = (Sgm A) . (i - (len (f - {p}))) by A24, A53, A55, A67;

A72: Sgm A is one-to-one by A11, FINSEQ_3:92;

i1 - (len (f - {p})) in dom (Sgm A) by A12, A70;

then (i1 - (len (f - {p}))) + (len (f - {p})) = (i - (len (f - {p}))) + (len (f - {p})) by A68, A71, A72;

hence a1 = a2 ; :: thesis: verum

end;then reconsider i1 = a2 as Nat ;

F . a2 = (Sgm A) . (i1 - (len (f - {p}))) by A24, A54, A70;

then A71: (Sgm A) . (i1 - (len (f - {p}))) = (Sgm A) . (i - (len (f - {p}))) by A24, A53, A55, A67;

A72: Sgm A is one-to-one by A11, FINSEQ_3:92;

i1 - (len (f - {p})) in dom (Sgm A) by A12, A70;

then (i1 - (len (f - {p}))) + (len (f - {p})) = (i - (len (f - {p}))) + (len (f - {p})) by A68, A71, A72;

hence a1 = a2 ; :: thesis: verum

then F . a1 in rng (Sgm A) by A24, A53, A67;

then A73: F . a1 in A by A11, FINSEQ_1:def 13;

now :: thesis: not a2 in Seg (len (f - {p}))

hence
a1 = a2
by A56, A69, XBOOLE_0:def 3; :: thesis: verumassume
a2 in Seg (len (f - {p}))
; :: thesis: contradiction

then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A24, A25, A21, A54, FINSEQ_3:40;

then F . a2 in rng (Sgm C) by FUNCT_1:3;

then F . a2 in C by A25, FINSEQ_1:def 13;

hence contradiction by A55, A73, XBOOLE_0:def 5; :: thesis: verum

end;then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A24, A25, A21, A54, FINSEQ_3:40;

then F . a2 in rng (Sgm C) by FUNCT_1:3;

then F . a2 in C by A25, FINSEQ_1:def 13;

hence contradiction by A55, A73, XBOOLE_0:def 5; :: thesis: verum

hence a1 = a2 by A57, A66, XBOOLE_0:def 3; :: thesis: verum

consider j being Nat such that

A74: j in dom F and

A75: F . j = i by A27, A19, FINSEQ_2:10;

A76: dom (Per (f,F)) = B by CALCUL_2:19

.= dom F by A24, A51, FINSEQ_1:def 3

.= dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A24, FINSEQ_1:def 3 ;

A77: now :: thesis: for k being Nat st k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) holds

(Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

then A92:
Per (f,F) = (f - {p}) ^ (IdFinS (p,(card A)))
by A76;(Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

let k be Nat; :: thesis: ( k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) implies (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k )

assume A78: k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) ; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

A79: k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A78, FINSEQ_1:def 3;

end;assume A78: k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) ; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

A79: k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A78, FINSEQ_1:def 3;

A80: now :: thesis: ( ex i being Nat st

( i in dom (IdFinS (p,(card A))) & k = (len (f - {p})) + i ) implies (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k )

( i in dom (IdFinS (p,(card A))) & k = (len (f - {p})) + i ) implies (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k )

A81:
k in dom (F * f)
by A76, A78, CALCUL_2:def 2;

given i being Nat such that A82: i in dom (IdFinS (p,(card A))) and

A83: k = (len (f - {p})) + i ; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

len (IdFinS (p,(card A))) = card A by CARD_1:def 7;

then A84: i <= card A by A82, FINSEQ_3:25;

then A85: k <= (card A) + (len (f - {p})) by A83, XREAL_1:6;

A86: 1 <= i by A82, FINSEQ_3:25;

then 1 + (len (f - {p})) <= k by A83, XREAL_1:6;

then A87: k in seq ((len (f - {p})),(card A)) by A85, CALCUL_2:1;

then F . k = (Sgm A) . (k - (len (f - {p}))) by A24, A79;

then F . k in rng (Sgm A) by A12, A87, FUNCT_1:3;

then F . k in A by A11, FINSEQ_1:def 13;

then f . (F . k) in {p} by FUNCT_1:def 7;

then f . (F . k) = p by TARSKI:def 1;

then (F * f) . k = p by A81, FUNCT_1:12;

then A88: (Per (f,F)) . k = p by CALCUL_2:def 2;

i in Seg (card A) by A86, A84, FINSEQ_1:1;

hence (Per (f,F)) . k = (IdFinS (p,(card A))) . i by A88, FUNCOP_1:7

.= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A82, A83, FINSEQ_1:def 7 ;

:: thesis: verum

end;given i being Nat such that A82: i in dom (IdFinS (p,(card A))) and

A83: k = (len (f - {p})) + i ; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

len (IdFinS (p,(card A))) = card A by CARD_1:def 7;

then A84: i <= card A by A82, FINSEQ_3:25;

then A85: k <= (card A) + (len (f - {p})) by A83, XREAL_1:6;

A86: 1 <= i by A82, FINSEQ_3:25;

then 1 + (len (f - {p})) <= k by A83, XREAL_1:6;

then A87: k in seq ((len (f - {p})),(card A)) by A85, CALCUL_2:1;

then F . k = (Sgm A) . (k - (len (f - {p}))) by A24, A79;

then F . k in rng (Sgm A) by A12, A87, FUNCT_1:3;

then F . k in A by A11, FINSEQ_1:def 13;

then f . (F . k) in {p} by FUNCT_1:def 7;

then f . (F . k) = p by TARSKI:def 1;

then (F * f) . k = p by A81, FUNCT_1:12;

then A88: (Per (f,F)) . k = p by CALCUL_2:def 2;

i in Seg (card A) by A86, A84, FINSEQ_1:1;

hence (Per (f,F)) . k = (IdFinS (p,(card A))) . i by A88, FUNCOP_1:7

.= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A82, A83, FINSEQ_1:def 7 ;

:: thesis: verum

now :: thesis: ( k in dom (f - {p}) implies (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k )

hence
(Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k
by A78, A80, FINSEQ_1:25; :: thesis: verumassume A89:
k in dom (f - {p})
; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

then A90: k in dom (Sgm C) by A26, A21, FINSEQ_1:def 3;

k in Seg (len (f - {p})) by A89, FINSEQ_1:def 3;

then A91: F . k = (Sgm C) . k by A24, A79;

k in dom (F * f) by A76, A78, CALCUL_2:def 2;

then (F * f) . k = f . ((Sgm C) . k) by A91, FUNCT_1:12;

hence (Per (f,F)) . k = f . ((Sgm C) . k) by CALCUL_2:def 2

.= ((Sgm C) * f) . k by A90, FUNCT_1:13

.= (f - {p}) . k by FINSEQ_3:def 1

.= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A89, FINSEQ_1:def 7 ;

:: thesis: verum

end;then A90: k in dom (Sgm C) by A26, A21, FINSEQ_1:def 3;

k in Seg (len (f - {p})) by A89, FINSEQ_1:def 3;

then A91: F . k = (Sgm C) . k by A24, A79;

k in dom (F * f) by A76, A78, CALCUL_2:def 2;

then (F * f) . k = f . ((Sgm C) . k) by A91, FUNCT_1:12;

hence (Per (f,F)) . k = f . ((Sgm C) . k) by CALCUL_2:def 2

.= ((Sgm C) * f) . k by A90, FUNCT_1:13

.= (f - {p}) . k by FINSEQ_3:def 1

.= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A89, FINSEQ_1:def 7 ;

:: thesis: verum

reconsider h = (f - {p}) ^ (IdFinS (p,(card A))) as FinSequence of CQC-WFF Al by A76, A77, FINSEQ_1:13;

(F * f) . j = p by A20, A74, A75, FUNCT_1:13;

then A93: h . j = p by A92, CALCUL_2:def 2;

A94: now :: thesis: not j in dom (f - {p})

j in dom f
by A74;assume A95:
j in dom (f - {p})
; :: thesis: contradiction

then (f - {p}) . j = p by A93, FINSEQ_1:def 7;

then A96: (f - {p}) . j in {p} by TARSKI:def 1;

A97: rng (f - {p}) = (rng f) \ {p} by FINSEQ_3:65;

(f - {p}) . j in rng (f - {p}) by A95, FUNCT_1:3;

hence contradiction by A96, A97, XBOOLE_0:def 5; :: thesis: verum

end;then (f - {p}) . j = p by A93, FINSEQ_1:def 7;

then A96: (f - {p}) . j in {p} by TARSKI:def 1;

A97: rng (f - {p}) = (rng f) \ {p} by FINSEQ_3:65;

(f - {p}) . j in rng (f - {p}) by A95, FUNCT_1:3;

hence contradiction by A96, A97, XBOOLE_0:def 5; :: thesis: verum

then j in dom h by A76, CALCUL_2:19;

then consider k being Nat such that

A98: k in dom (IdFinS (p,(card A))) and

j = (len (f - {p})) + k by A94, FINSEQ_1:25;

reconsider g = f - {p} as FinSequence of CQC-WFF Al by FINSEQ_3:86;

( 1 <= k & k <= len (IdFinS (p,(card A))) ) by A98, FINSEQ_3:25;

then 1 <= len (IdFinS (p,(card A))) by XXREAL_0:2;

then A99: 1 <= card A by CARD_1:def 7;

|- h ^ <*('not' p)*> by A9, A92, CALCUL_2:30;

then A100: |- (g ^ <*p*>) ^ <*('not' p)*> by A99, CALCUL_2:32;

( rng g = (rng f) \ {p} & (rng f) \ {p} c= (X \/ {p}) \ {p} ) by A8, FINSEQ_3:65, XBOOLE_1:33;

then A101: rng g c= X \ {p} by XBOOLE_1:40;

X \ {p} c= X by XBOOLE_1:36;

then A102: rng g c= X by A101;

|- (g ^ <*('not' p)*>) ^ <*('not' p)*> by CALCUL_2:21;

then |- g ^ <*('not' p)*> by A100, CALCUL_2:26;

hence X |- 'not' p by A102; :: thesis: verum