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

for p, q being Element of CQC-WFF Al st X \/ {p} |- q holds

ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

let X be Subset of (CQC-WFF Al); :: thesis: for p, q being Element of CQC-WFF Al st X \/ {p} |- q holds

ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

let p, q be Element of CQC-WFF Al; :: thesis: ( X \/ {p} |- q implies ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) )

assume X \/ {p} |- q ; :: thesis: ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

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

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

A2: |- f ^ <*q*> ;

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A3; :: thesis: verum

for p, q being Element of CQC-WFF Al st X \/ {p} |- q holds

ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

let X be Subset of (CQC-WFF Al); :: thesis: for p, q being Element of CQC-WFF Al st X \/ {p} |- q holds

ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

let p, q be Element of CQC-WFF Al; :: thesis: ( X \/ {p} |- q implies ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) )

assume X \/ {p} |- q ; :: thesis: ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

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

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

A2: |- f ^ <*q*> ;

A3: now :: thesis: ( not rng f c= X implies ex g, g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) )

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) )

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

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

A c= B by RELAT_1:132;

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

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

then consider a being object such that

A11: a in rng f and

A12: not a in X ;

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

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

then consider i being Nat such that

A13: i in B and

A14: f . i = p by A11, 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}))) ) );

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

A16: 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]

A18: ( 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(A16);

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

A21: 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 A46: dom F = B by A18, FINSEQ_1:def 3;

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

rng F c= B ;

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

F is one-to-one

consider j being Nat such that

A68: j in dom F and

A69: F . j = i by A21, A13, FINSEQ_2:10;

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

.= dom F by A18, A45, FINSEQ_1:def 3

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

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

(F * f) . j = p by A14, A68, A69, FUNCT_1:13;

then A87: h . j = p by A86, CALCUL_2:def 2;

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

then consider k being Nat such that

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

j = (len (f - {p})) + k by A88, 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 A92, FINSEQ_3:25;

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

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

|- h ^ <*q*> by A2, A86, CALCUL_2:30;

then A94: |- (g ^ <*p*>) ^ <*q*> by A93, CALCUL_2:32;

take g = g; :: thesis: ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

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

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

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

hence ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A94, A95, XBOOLE_1:1; :: 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)));

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

A c= B by RELAT_1:132;

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

A6: 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: ex g, g being FinSequence of CQC-WFF Al st i - (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 A7: i in seq ((len (f - {p})),(card A)) ; :: thesis: i - (len (f - {p})) in dom (Sgm A)

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

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

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

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

0 <= j by A8, XREAL_1:19;

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

j in Seg (card A) by A9, A10, FINSEQ_1:1;

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

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

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

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

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

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

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

0 <= j by A8, XREAL_1:19;

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

j in Seg (card A) by A9, A10, FINSEQ_1:1;

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

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

then consider a being object such that

A11: a in rng f and

A12: not a in X ;

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

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

then consider i being Nat such that

A13: i in B and

A14: f . i = p by A11, FINSEQ_2:10;

reconsider C = B \ A as finite set ;

defpred S

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

A16: 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 A17:
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 A17, 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

A18: ( 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 A19:
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 A20: dom (Sgm C) = Seg (card C) by FINSEQ_3:40;

A21: rng F = B

proof

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

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

end;

A45: 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

A22: i in dom F and

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

hence a in B by A24, A25, XBOOLE_0:def 3; :: thesis: verum

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

then consider i being Nat such that

A22: i in dom F and

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

A24: 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 A18, A19, A15, A22, A23, FINSEQ_3:40;

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

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

hence a in B ; :: thesis: verum

end;then ( a = (Sgm C) . i & i in dom (Sgm C) ) by A18, A19, A15, A22, A23, FINSEQ_3:40;

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

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

hence a in B ; :: thesis: verum

A25: 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 A4, A18, A22, Lm1;A26:
rng (Sgm A) = A
by A5, FINSEQ_1:def 13;

A27: A c= B by RELAT_1:132;

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

then a = (Sgm A) . (i - (len (f - {p}))) by A18, A22, A23;

then a in A by A6, A28, A26, FUNCT_1:3;

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

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

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

then a = (Sgm A) . (i - (len (f - {p}))) by A18, A22, A23;

then a in A by A6, A28, A26, FUNCT_1:3;

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

hence a in B by A24, A25, 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 A29: a in B ; :: thesis: a in rng F

A30: 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 A29, XBOOLE_0:def 5;

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

then consider i being Nat such that

A32: i in dom (Sgm C) and

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

A34: 1 <= i by A32, FINSEQ_3:25;

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

then A35: i <= len (f - {p}) by A32, 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 A35, XXREAL_0:2;

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

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

then a = F . i by A18, A33, A36;

hence a in rng F by A18, A36, FUNCT_1:3; :: thesis: verum

end;

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

b in Seg (len f)

then A31:
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 A29, XBOOLE_0:def 5;

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

then consider i being Nat such that

A32: i in dom (Sgm C) and

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

A34: 1 <= i by A32, FINSEQ_3:25;

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

then A35: i <= len (f - {p}) by A32, 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 A35, XXREAL_0:2;

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

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

then a = F . i by A18, A33, A36;

hence a in rng F by A18, A36, FUNCT_1:3; :: thesis: verum

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

hence
a in rng F
by A30; :: thesis: verumassume A37:
a in A
; :: thesis: a in rng F

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

then consider i being Nat such that

A38: i in dom (Sgm A) and

A39: (Sgm A) . i = a by A37, FINSEQ_2:10;

reconsider i = i as Nat ;

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

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

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

then A40: 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 A41: i + (len (f - {p})) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by FINSEQ_1:22;

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

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

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

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

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

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

then A44: 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 A39;

then a = F . (i + (len (f - {p}))) by A18, A43, A44;

hence a in rng F by A18, A44, FUNCT_1:3; :: thesis: verum

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

then consider i being Nat such that

A38: i in dom (Sgm A) and

A39: (Sgm A) . i = a by A37, FINSEQ_2:10;

reconsider i = i as Nat ;

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

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

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

then A40: 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 A41: i + (len (f - {p})) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by FINSEQ_1:22;

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

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

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

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

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

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

then A44: 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 A39;

then a = F . (i + (len (f - {p}))) by A18, A43, A44;

hence a in rng F by A18, A44, 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 A46: dom F = B by A18, FINSEQ_1:def 3;

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

rng F c= B ;

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

F is one-to-one

proof

then reconsider F = F as Permutation of (dom f) by A21, 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

A47: a1 in dom F and

A48: a2 in dom F and

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

A50: a2 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A4, A18, A48, Lm1;

hence a1 = a2 by A51, A60, XBOOLE_0:def 3; :: thesis: verum

end;assume that

A47: a1 in dom F and

A48: a2 in dom F and

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

A50: a2 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A4, A18, A48, Lm1;

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

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

then A53: a1 in dom (Sgm C) by A19, A15, FINSEQ_3:40;

F . a1 = (Sgm C) . a1 by A18, A47, A52;

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

then A54: F . a1 in C by A19, FINSEQ_1:def 13;

end;then A53: a1 in dom (Sgm C) by A19, A15, FINSEQ_3:40;

F . a1 = (Sgm C) . a1 by A18, A47, A52;

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

then A54: F . a1 in C by A19, FINSEQ_1:def 13;

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

assume A56:
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 A6, A56, FUNCT_1:3;

then F . a2 in rng (Sgm A) by A18, A48, A56;

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

hence contradiction by A49, A54, XBOOLE_0:def 5; :: thesis: verum

end;then reconsider i = a2 as Nat ;

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

then F . a2 in rng (Sgm A) by A18, A48, A56;

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

hence contradiction by A49, A54, XBOOLE_0:def 5; :: thesis: verum

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

hence
a1 = a2
by A50, A55, XBOOLE_0:def 3; :: thesis: verumassume A57:
a2 in Seg (len (f - {p}))
; :: thesis: a1 = a2

then F . a2 = (Sgm C) . a2 by A18, A48;

then A58: (Sgm C) . a1 = (Sgm C) . a2 by A18, A47, A49, A52;

A59: Sgm C is one-to-one by A19, FINSEQ_3:92;

a2 in dom (Sgm C) by A19, A15, A57, FINSEQ_3:40;

hence a1 = a2 by A53, A58, A59; :: thesis: verum

end;then F . a2 = (Sgm C) . a2 by A18, A48;

then A58: (Sgm C) . a1 = (Sgm C) . a2 by A18, A47, A49, A52;

A59: Sgm C is one-to-one by A19, FINSEQ_3:92;

a2 in dom (Sgm C) by A19, A15, A57, FINSEQ_3:40;

hence a1 = a2 by A53, A58, A59; :: thesis: verum

A60: 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 A4, A18, A47, Lm1;assume A61:
a1 in seq ((len (f - {p})),(card A))
; :: thesis: a1 = a2

then reconsider i = a1 as Nat ;

A62: i - (len (f - {p})) in dom (Sgm A) by A6, A61;

then F . a1 in rng (Sgm A) by A18, A47, A61;

then A67: F . a1 in A by A5, FINSEQ_1:def 13;

end;then reconsider i = a1 as Nat ;

A62: i - (len (f - {p})) in dom (Sgm A) by A6, A61;

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

(Sgm A) . (i - (len (f - {p}))) in rng (Sgm A)
by A6, A61, FUNCT_1:3;assume A64:
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 A18, A48, A64;

then A65: (Sgm A) . (i1 - (len (f - {p}))) = (Sgm A) . (i - (len (f - {p}))) by A18, A47, A49, A61;

A66: Sgm A is one-to-one by A5, FINSEQ_3:92;

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

then (i1 - (len (f - {p}))) + (len (f - {p})) = (i - (len (f - {p}))) + (len (f - {p})) by A62, A65, A66;

hence a1 = a2 ; :: thesis: verum

end;then reconsider i1 = a2 as Nat ;

F . a2 = (Sgm A) . (i1 - (len (f - {p}))) by A18, A48, A64;

then A65: (Sgm A) . (i1 - (len (f - {p}))) = (Sgm A) . (i - (len (f - {p}))) by A18, A47, A49, A61;

A66: Sgm A is one-to-one by A5, FINSEQ_3:92;

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

then (i1 - (len (f - {p}))) + (len (f - {p})) = (i - (len (f - {p}))) + (len (f - {p})) by A62, A65, A66;

hence a1 = a2 ; :: thesis: verum

then F . a1 in rng (Sgm A) by A18, A47, A61;

then A67: F . a1 in A by A5, FINSEQ_1:def 13;

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

hence
a1 = a2
by A50, A63, 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 A18, A19, A15, A48, FINSEQ_3:40;

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

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

hence contradiction by A49, A67, XBOOLE_0:def 5; :: thesis: verum

end;then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A18, A19, A15, A48, FINSEQ_3:40;

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

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

hence contradiction by A49, A67, XBOOLE_0:def 5; :: thesis: verum

hence a1 = a2 by A51, A60, XBOOLE_0:def 3; :: thesis: verum

consider j being Nat such that

A68: j in dom F and

A69: F . j = i by A21, A13, FINSEQ_2:10;

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

.= dom F by A18, A45, FINSEQ_1:def 3

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

A71: 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 A86:
Per (f,F) = (f - {p}) ^ (IdFinS (p,(card A)))
by A70;(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 A72: k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) ; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

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

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

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

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

A75:
k in dom (F * f)
by A70, A72, CALCUL_2:def 2;

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

A77: 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 A78: i <= card A by A76, FINSEQ_3:25;

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

A80: 1 <= i by A76, FINSEQ_3:25;

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

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

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

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

then F . k in A by A5, 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 A75, FUNCT_1:12;

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

i in Seg (card A) by A80, A78, FINSEQ_1:1;

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

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

:: thesis: verum

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

A77: 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 A78: i <= card A by A76, FINSEQ_3:25;

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

A80: 1 <= i by A76, FINSEQ_3:25;

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

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

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

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

then F . k in A by A5, 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 A75, FUNCT_1:12;

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

i in Seg (card A) by A80, A78, FINSEQ_1:1;

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

.= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A76, A77, 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 A72, A74, FINSEQ_1:25; :: thesis: verumassume A83:
k in dom (f - {p})
; :: thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k

then A84: k in dom (Sgm C) by A20, A15, FINSEQ_1:def 3;

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

then A85: F . k = (Sgm C) . k by A18, A73;

k in dom (F * f) by A70, A72, CALCUL_2:def 2;

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

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

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

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

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

:: thesis: verum

end;then A84: k in dom (Sgm C) by A20, A15, FINSEQ_1:def 3;

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

then A85: F . k = (Sgm C) . k by A18, A73;

k in dom (F * f) by A70, A72, CALCUL_2:def 2;

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

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

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

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

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

:: thesis: verum

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

(F * f) . j = p by A14, A68, A69, FUNCT_1:13;

then A87: h . j = p by A86, CALCUL_2:def 2;

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

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

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

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

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

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

hence contradiction by A90, A91, XBOOLE_0:def 5; :: thesis: verum

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

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

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

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

hence contradiction by A90, A91, XBOOLE_0:def 5; :: thesis: verum

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

then consider k being Nat such that

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

j = (len (f - {p})) + k by A88, 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 A92, FINSEQ_3:25;

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

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

|- h ^ <*q*> by A2, A86, CALCUL_2:30;

then A94: |- (g ^ <*p*>) ^ <*q*> by A93, CALCUL_2:32;

take g = g; :: thesis: ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

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

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

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

hence ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A94, A95, XBOOLE_1:1; :: thesis: verum

now :: thesis: ( rng f c= X implies ex f, g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) )

hence
ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) )

assume A96:
rng f c= X
; :: thesis: ex f, g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

take f = f; :: thesis: ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

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

hence ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A96; :: thesis: verum

end;( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

take f = f; :: thesis: ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )

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

hence ex g being FinSequence of CQC-WFF Al st

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A96; :: thesis: verum

( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A3; :: thesis: verum