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

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

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 A c= Seg (len f) by FINSEQ_1:def 3;
then a5: A is included_in_Seg by FINSEQ_1:def 13;

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)

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;

assume not rng f c= X ; :: thesis: ex g, g being FinSequence of CQC-WFF Al st
( 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₁[ 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₁[k,a]

proof

let k be Nat; :: thesis: ( k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) implies ex a being object st S₁[k,a] )
assume k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) ; :: thesis: ex a being object st S₁[k,a]

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

assume A17: k in Seg (len (f - {p})) ; :: thesis: ex a being set st S₁[k,a]
take a = (Sgm (B \ A)) . k; :: thesis: S₁[k,a]
Seg (len (f - {p})) misses seq ((len (f - {p})),(card A)) by CALCUL_2:8;
hence S₁[k,a] by A17, XBOOLE_0:3; :: thesis: verum

end;

hence ex a being object st S₁[k,a] ; :: thesis: verum

end;

consider F being FinSequence such that
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₁[k,F . k] ) ) from FINSEQ_1:sch 1(A16);
A20: dom (Sgm C) = Seg (card C) by FINSEQ_3:40;
A21: rng F = B

proof

now :: thesis: for a being object st a in rng F holds
a 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;

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, A15, A22, A23, FINSEQ_3:40;
then a in rng (Sgm C) by FUNCT_1:3;
then a in C by FINSEQ_1:def 14;
hence a in B ; :: thesis: verum

end;

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

A26: rng (Sgm A) = A by a5, FINSEQ_1:def 14;
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;

i in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A4, A18, A22, Lm1;
hence a in B by A24, A25, XBOOLE_0:def 3; :: thesis: verum

end;

hence rng F c= B ; :: according to XBOOLE_0:def 10 :: thesis: B c= rng F
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 FINSEQ_1:def 14;
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: ( a in A implies a in rng F )

assume A37: a in A ; :: thesis: a in rng F
rng (Sgm A) = A by a5, FINSEQ_1:def 14;
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;

hence a in rng F by A30; :: thesis: verum

end;

A45: len ((f - {p}) ^ (IdFinS (p,(card A)))) = (len (f - {p})) + (len (IdFinS (p,(card A)))) by FINSEQ_1:22
.= ((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

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;

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 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 FINSEQ_1:def 14;

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 14;
hence contradiction by A49, A54, XBOOLE_0:def 5; :: thesis: verum

end;

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

assume 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 FINSEQ_3:92;
a2 in dom (Sgm C) by A15, A57, FINSEQ_3:40;
hence a1 = a2 by A53, A58, A59; :: thesis: verum

end;

hence a1 = a2 by A50, A55, XBOOLE_0:def 3; :: thesis: verum

end;

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

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;

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

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;

(Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A6, A61, FUNCT_1:3;
then F . a1 in rng (Sgm A) by A18, A47, A61;
then A67: F . a1 in A by a5, FINSEQ_1:def 14;

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

assume a2 in Seg (len (f - {p})) ; :: thesis: contradiction
then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A18, A15, A48, FINSEQ_3:40;
then F . a2 in rng (Sgm C) by FUNCT_1:3;
then F . a2 in C by FINSEQ_1:def 14;
hence contradiction by A49, A67, XBOOLE_0:def 5; :: thesis: verum

end;

hence a1 = a2 by A50, A63, XBOOLE_0:def 3; :: thesis: verum

end;

a1 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A4, A18, A47, Lm1;
hence a1 = a2 by A51, A60, XBOOLE_0:def 3; :: thesis: verum

end;

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

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;

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 )

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

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

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

hence (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A72, A74, FINSEQ_1:25; :: thesis: verum

end;

then A86: Per (f,F) = (f - {p}) ^ (IdFinS (p,(card A))) by A70;
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})

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;

j in dom f by A68;
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;

now :: thesis: ( rng f c= X implies ex f, 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;

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