let Al be QC-alphabet ; 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); 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; ( X \/ {p} |- q implies ex g being FinSequence of CQC-WFF Al st
( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) )
assume
X \/ {p} |- q
; 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 ( 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 A5:
A c= Seg (len f)
by FINSEQ_1:def 3;
assume
not
rng f c= X
;
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 S1[
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
S1[
k,
a]
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
S1[
k,
F . k] ) )
from FINSEQ_1:sch 1(A16);
then A19:
C c= Seg (len f)
;
then A20:
dom (Sgm C) = Seg (card C)
by FINSEQ_3:40;
A21:
rng F = B
proof
hence
rng F c= B
;
XBOOLE_0:def 10 B c= rng F
let a be
object ;
TARSKI:def 3 ( not a in B or a in rng F )
assume A29:
a in B
;
a in rng F
A30:
now ( not a in A implies a in rng F )then A31:
C c= Seg (len f)
;
assume
not
a in A
;
a in rng Fthen
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;
verum end;
now ( a in A implies a in rng F )assume A37:
a in A
;
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;
verum end;
hence
a in rng F
by A30;
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 ;
FUNCT_1:def 4 ( 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
;
a1 = a2
A50:
a2 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A)))
by A4, A18, A48, Lm1;
A51:
now ( a1 in Seg (len (f - {p})) implies a1 = a2 )assume A52:
a1 in Seg (len (f - {p}))
;
a1 = a2then 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;
now ( a2 in Seg (len (f - {p})) implies a1 = a2 )assume A57:
a2 in Seg (len (f - {p}))
;
a1 = a2then
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;
verum end; hence
a1 = a2
by A50, A55, XBOOLE_0:def 3;
verum end;
A60:
now ( a1 in seq ((len (f - {p})),(card A)) implies a1 = a2 )assume A61:
a1 in seq (
(len (f - {p})),
(card A))
;
a1 = a2then reconsider i =
a1 as
Nat ;
A62:
i - (len (f - {p})) in dom (Sgm A)
by A6, A61;
A63:
now ( a2 in seq ((len (f - {p})),(card A)) implies a1 = a2 )assume A64:
a2 in seq (
(len (f - {p})),
(card A))
;
a1 = a2then 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
;
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 13;
hence
a1 = a2
by A50, A63, XBOOLE_0:def 3;
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;
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 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)))) . klet k be
Nat;
( 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))))
;
(Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . kA73:
k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A)))))
by A72, FINSEQ_1:def 3;
A74:
now ( 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
;
(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
;
verum end; now ( k in dom (f - {p}) implies (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k )assume A83:
k in dom (f - {p})
;
(Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . kthen 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
;
verum end; hence
(Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k
by A72, A74, FINSEQ_1:25;
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;
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;
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;
verum end;
hence
ex g being FinSequence of CQC-WFF Al st
( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )
by A3; verum