set T = F2() -tuples_on F1();
set XX = { F where F is Element of F2() -tuples_on F1() : P1[F] } ;
per cases
( { F where F is Element of F2() -tuples_on F1() : P1[F] } is empty or not { F where F is Element of F2() -tuples_on F1() : P1[F] } is empty )
;
suppose
not
{ F where F is Element of F2() -tuples_on F1() : P1[F] } is
empty
;
ex C being Cardinal st F2() *` C = card { F where F is Element of F2() -tuples_on F1() : P1[F] } deffunc H1(
object )
-> set =
{ (p ^ q) where p, q is Element of F1() * : q ^ p = $1 } ;
A4:
for
x being
object st
x in { F where F is Element of F2() -tuples_on F1() : P1[F] } holds
H1(
x)
in bool { F where F is Element of F2() -tuples_on F1() : P1[F] }
consider F being
Function of
{ F where F is Element of F2() -tuples_on F1() : P1[F] } ,
(bool { F where F is Element of F2() -tuples_on F1() : P1[F] } ) such that A11:
for
x being
object st
x in { F where F is Element of F2() -tuples_on F1() : P1[F] } holds
F . x = H1(
x)
from FUNCT_2:sch 2(A4);
set FF =
F ~ ;
A12:
dom F = { F where F is Element of F2() -tuples_on F1() : P1[F] }
by FUNCT_2:def 1;
A13:
F2()
in Seg F2()
by FINSEQ_1:3;
for
x being
object st
x in rng F holds
card (Im ((F ~),x)) = F2()
proof
let x be
object ;
( x in rng F implies card (Im ((F ~),x)) = F2() )
assume
x in rng F
;
card (Im ((F ~),x)) = F2()
then consider y being
object such that A14:
y in dom F
and A15:
F . y = x
by FUNCT_1:def 3;
consider p being
Element of
F2()
-tuples_on F1()
such that A16:
y = p
and A17:
P1[
p]
by A14, A12;
A18:
x = H1(
p)
by A14, A15, A16, A11;
defpred S1[
object ,
object ]
means for
i being
Nat st
i = $1 holds
$2
= (p /^ i) ^ (p | i);
A19:
len p = F2()
by CARD_1:def 7;
then
(
p /^ F2()
= {} &
p | F2()
= p )
by RFINSEQ:27, FINSEQ_1:58;
then A20:
p = (p /^ F2()) ^ (p | F2())
by FINSEQ_1:34;
A21:
for
i being
object st
i in Seg F2() holds
ex
q being
object st
(
q in Im (
(F ~),
x) &
S1[
i,
q] )
proof
let i be
object ;
( i in Seg F2() implies ex q being object st
( q in Im ((F ~),x) & S1[i,q] ) )
assume
i in Seg F2()
;
ex q being object st
( q in Im ((F ~),x) & S1[i,q] )
then reconsider I =
i as
Nat ;
set q =
p /^ I;
take qp =
(p /^ I) ^ (p | I);
( qp in Im ((F ~),x) & S1[i,qp] )
A22:
p = (p | I) ^ (p /^ I)
by RFINSEQ:8;
then
len p = (len (p | I)) + (len (p /^ I))
by FINSEQ_1:22;
then A23:
len qp = F2()
by FINSEQ_1:22, A19;
then A24:
qp is
Element of
F2()
-tuples_on F1()
by FINSEQ_2:92;
A25:
H1(
p)
c= H1(
qp)
proof
let t be
object ;
TARSKI:def 3 ( not t in H1(p) or t in H1(qp) )
assume
t in H1(
p)
;
t in H1(qp)
then consider t1,
t2 being
Element of
F1()
* such that A26:
t = t1 ^ t2
and A27:
p = t2 ^ t1
;
reconsider t12 =
t as
Element of
F1()
* by A26, FINSEQ_1:def 11;
set LT =
len t1;
A28:
t12 = (t12 | (len t1)) ^ (t12 /^ (len t1))
by RFINSEQ:8;
t12 | (len t1) = t1
by A26, FINSEQ_5:23;
then
(t12 /^ (len t1)) ^ (t12 | (len t1)) = (p /^ F2()) ^ (p | F2())
by A27, A28, A26, FINSEQ_1:33, A20;
then A29:
ex
k2 being
Nat st
(t12 /^ k2) ^ (t12 | k2) = p
by Th5;
(
qp /^ F2()
= {} &
qp | F2()
= qp )
by A23, RFINSEQ:27, FINSEQ_1:58;
then
(p /^ I) ^ (p | I) = (qp /^ F2()) ^ (qp | F2())
by FINSEQ_1:34;
then
ex
k1 being
Nat st
(qp /^ k1) ^ (qp | k1) = p
by Th5;
then consider k3 being
Nat such that A30:
(t12 /^ k3) ^ (t12 | k3) = qp
by A29, Th5;
(
t12 /^ k3 in F1()
* &
t12 | k3 in F1()
* )
by FINSEQ_1:def 11;
then
(t12 | k3) ^ (t12 /^ k3) in H1(
qp)
by A30;
hence
t in H1(
qp)
by RFINSEQ:8;
verum
end;
P1[
qp]
by A1, A17, A22;
then A31:
qp in dom F
by A24, A12;
then
F . qp = H1(
qp)
by A11;
then
[qp,H1(qp)] in F
by FUNCT_1:def 2, A31;
then A32:
[H1(qp),qp] in F ~
by RELAT_1:def 7;
H1(
qp)
c= H1(
p)
then
H1(
qp)
= H1(
p)
by A25;
hence
(
qp in Im (
(F ~),
x) &
S1[
i,
qp] )
by A32, RELAT_1:169, A18;
verum
end;
consider PR being
Function of
(Seg F2()),
(Im ((F ~),x)) such that A37:
for
i being
object st
i in Seg F2() holds
S1[
i,
PR . i]
from FUNCT_2:sch 1(A21);
[y,x] in F
by A14, A15, FUNCT_1:def 2;
then
[x,y] in F ~
by RELAT_1:def 7;
then
y in Im (
(F ~),
x)
by RELAT_1:169;
then A38:
dom PR = Seg F2()
by FUNCT_2:def 1;
Im (
(F ~),
x)
c= rng PR
proof
let z be
object ;
TARSKI:def 3 ( not z in Im ((F ~),x) or z in rng PR )
assume
z in Im (
(F ~),
x)
;
z in rng PR
then
[x,z] in F ~
by RELAT_1:169;
then A39:
[z,x] in F
by RELAT_1:def 7;
then A40:
z in dom F
by XTUPLE_0:def 12;
then A41:
F . z = H1(
z)
by A11;
consider Z being
Element of
F2()
-tuples_on F1()
such that A42:
z = Z
and
P1[
Z]
by A40, A12;
A43:
(
Z in F1()
* &
<*> F1()
in F1()
* )
by FINSEQ_1:def 11;
A44:
(
Z = Z ^ (<*> F1()) &
(<*> F1()) ^ Z = Z )
by FINSEQ_1:34;
x is
set
by TARSKI:1;
then
F . z = x
by A40, A39, FUNCT_1:def 2;
then
z in H1(
p)
by A44, A43, A41, A42, A18;
then consider z1,
z2 being
Element of
F1()
* such that A45:
z = z1 ^ z2
and A46:
z2 ^ z1 = p
;
set L =
len z2;
A47:
p | (len z2) = z2
by A46, FINSEQ_5:23;
(len z2) + (len z1) = len p
by A46, FINSEQ_1:22;
then A48:
len z2 <= len p
by NAT_1:11;
A49:
p = (p | (len z2)) ^ (p /^ (len z2))
by RFINSEQ:8;
then A50:
z1 = p /^ (len z2)
by A47, A46, FINSEQ_1:33;
end;
then A53:
rng PR = Im (
(F ~),
x)
;
PR is
one-to-one
proof
let i1,
i2 be
object ;
FUNCT_1:def 4 ( not i1 in dom PR or not i2 in dom PR or not PR . i1 = PR . i2 or i1 = i2 )
assume that A54:
i1 in dom PR
and A55:
i2 in dom PR
and A56:
PR . i1 = PR . i2
;
i1 = i2
reconsider i1 =
i1,
i2 =
i2 as
Nat by A54, A55, A38;
A57:
1
<= i1
by A54, FINSEQ_1:1;
A58:
1
<= i2
by A55, FINSEQ_1:1;
A59:
i2 <= F2()
by A55, FINSEQ_1:1;
A60:
(
PR . i2 = (p /^ i2) ^ (p | i2) &
PR . i1 = (p /^ i1) ^ (p | i1) )
by A55, A37, A54;
then reconsider P1 =
PR . i1,
P2 =
PR . i2 as
Element of
F1()
* by FINSEQ_1:def 11;
A61:
i1 <= F2()
by A54, FINSEQ_1:1;
A62:
F2()
- 1
< F2()
- 0
by XREAL_1:15;
per cases
( i1 <= i2 or i2 <= i1 )
;
suppose
i1 <= i2
;
i1 = i2then A63:
(
p = (p /^ (i2 -' i1)) ^ (p | (i2 -' i1)) &
i2 -' i1 = i2 - i1 )
by Th3, A19, A59, A60, A56, XREAL_1:233;
i2 - i1 <= F2()
- 1
by A57, A59, XREAL_1:13;
then
i2 - i1 < F2()
by XXREAL_0:2, A62;
then
i2 - i1 = 0
by A17, A2, A63;
hence
i1 = i2
;
verum end; suppose
i2 <= i1
;
i1 = i2then A64:
(
p = (p /^ (i1 -' i2)) ^ (p | (i1 -' i2)) &
i1 -' i2 = i1 - i2 )
by Th3, A19, A61, A60, A56, XREAL_1:233;
i1 - i2 <= F2()
- 1
by A61, A58, XREAL_1:13;
then
i1 - i2 < F2()
by XXREAL_0:2, A62;
then
i1 - i2 = 0
by A17, A2, A64;
hence
i1 = i2
;
verum end; end;
end;
hence card (Im ((F ~),x)) =
card (Seg F2())
by A53, A38, WELLORD2:def 4, CARD_1:5
.=
F2()
by FINSEQ_1:57
;
verum
end; then A65:
card (F ~) = (card ((F ~) | ((dom (F ~)) \ (rng F)))) +` (F2() *` (card (rng F)))
by SIMPLEX1:1;
dom (F ~) = rng F
by RELAT_1:20;
then
(dom (F ~)) \ (rng F) = {}
by XBOOLE_1:37;
then
card ((F ~) | ((dom (F ~)) \ (rng F))) = 0
;
then F2()
*` (card (rng F)) =
card (F ~)
by A65, CARD_2:18
.=
card F
by Th1
.=
card { F where F is Element of F2() -tuples_on F1() : P1[F] }
by A12, CARD_1:62
;
hence
ex
C being
Cardinal st
F2()
*` C = card { F where F is Element of F2() -tuples_on F1() : P1[F] }
;
verum end; end;