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 A3: { F where F is Element of F2() -tuples_on F1() : P1[F] } is empty ; :: thesis: ex C being Cardinal st F2() *` C = card { F where F is Element of F2() -tuples_on F1() : P1[F] }
0 = F2() *` 0 by CARD_2:20;
hence ex C being Cardinal st F2() *` C = card { F where F is Element of F2() -tuples_on F1() : P1[F] } by A3; :: thesis: verum
end;
suppose not { F where F is Element of F2() -tuples_on F1() : P1[F] } is empty ; :: thesis: 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] }
proof
let x be object ; :: thesis: ( x in { F where F is Element of F2() -tuples_on F1() : P1[F] } implies H1(x) in bool { F where F is Element of F2() -tuples_on F1() : P1[F] } )
assume x in { F where F is Element of F2() -tuples_on F1() : P1[F] } ; :: thesis: H1(x) in bool { F where F is Element of F2() -tuples_on F1() : P1[F] }
then consider pq being Element of F2() -tuples_on F1() such that
A5: x = pq and
A6: P1[pq] ;
 H1(x) c= { F where F is Element of F2() -tuples_on F1() : P1[F] }
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H1(x) or y in { F where F is Element of F2() -tuples_on F1() : P1[F] } )
A7: len pq = F2() by CARD_1:def 7;
assume y in H1(x) ; :: thesis: y in { F where F is Element of F2() -tuples_on F1() : P1[F] }
then consider p1, q1 being Element of F1() * such that
A8: y = p1 ^ q1 and
A9: q1 ^ p1 = pq by A5;
len pq = (len q1) + (len p1) by A9, FINSEQ_1:22;
then len (p1 ^ q1) = F2() by A7, FINSEQ_1:22;
then A10: p1 ^ q1 is Element of F2() -tuples_on F1() by FINSEQ_2:92;
P1[p1 ^ q1] by A6, A9, A1;
hence y in { F where F is Element of F2() -tuples_on F1() : P1[F] } by A10, A8; :: thesis: verum
end;
hence H1(x) in bool { F where F is Element of F2() -tuples_on F1() : P1[F] } ; :: thesis: verum
end;
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 ; :: thesis: ( x in rng F implies card (Im ((F ~),x)) = F2() )
assume x in rng F ; :: thesis: 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 ; :: thesis: ( i in Seg F2() implies ex q being object st
( q in Im ((F ~),x) & S1[i,q] ) )
assume i in Seg F2() ; :: thesis: 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); :: thesis: ( 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 ; :: according to TARSKI:def 3 :: thesis: ( not t in H1(p) or t in H1(qp) )
assume t in H1(p) ; :: thesis: 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; :: thesis: 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)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in H1(qp) or t in H1(p) )
assume t in H1(qp) ; :: thesis: t in H1(p)
then consider t1, t2 being Element of F1() * such that
A33: t = t1 ^ t2 and
A34: (p /^ I) ^ (p | I) = t2 ^ t1 ;
reconsider t12 = t as Element of F1() * by A33, FINSEQ_1:def 11;
set LT = len t1;
A35: t12 = (t12 | (len t1)) ^ (t12 /^ (len t1)) by RFINSEQ:8;
t12 | (len t1) = t1 by A33, FINSEQ_5:23;
then (t12 /^ (len t1)) ^ (t12 | (len t1)) = (p /^ I) ^ (p | I) by A34, A35, A33, FINSEQ_1:33;
then consider k being Nat such that
A36: (t12 /^ k) ^ (t12 | k) = p by Th5;
( t12 /^ k in F1() * & t12 | k in F1() * ) by FINSEQ_1:def 11;
then (t12 | k) ^ (t12 /^ k) in H1(p) by A36;
hence t in H1(p) by RFINSEQ:8; :: thesis: verum
end;
then H1(qp) = H1(p) by A25;
hence ( qp in Im ((F ~),x) & S1[i,qp] ) by A32, RELAT_1:169, A18; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not z in Im ((F ~),x) or z in rng PR )
assume z in Im ((F ~),x) ; :: thesis: 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 ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: i1 = i2
then 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 ; :: thesis: verum
end;
suppose i2 <= i1 ; :: thesis: i1 = i2
then 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 ; :: thesis: 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 ;
:: thesis: 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] } ; :: thesis: verum
end;
end;