set T = F₂() -tuples_on F₁();
set XX = { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } ;

per cases ( { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } is empty or not { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } is empty ) ;

suppose A3: { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } is empty ; :: thesis: ex C being Cardinal st F₂() *` C = card { F where F is Element of F₂() -tuples_on F₁() : P₁[F] }

0 = F₂() *` 0 by CARD_2:20;
hence ex C being Cardinal st F<sub>2</sub>() *` C = card { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } by A3; :: thesis: verum

end;

suppose not { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } is empty ; :: thesis: ex C being Cardinal st F₂() *` C = card { F where F is Element of F₂() -tuples_on F₁() : P₁[F] }

deffunc H₁( object ) -> set = { (p ^ q) where p, q is Element of F₁() * : q ^ p = $1 } ;
A4: for x being object st x in { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } holds
H₁(x) in bool { F where F is Element of F₂() -tuples_on F₁() : P₁[F] }

proof

let x be object ; :: thesis: ( x in { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } implies H₁(x) in bool { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } )
assume x in { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } ; :: thesis: H₁(x) in bool { F where F is Element of F₂() -tuples_on F₁() : P₁[F] }
then consider pq being Element of F₂() -tuples_on F₁() such that
A5: x = pq and
A6: P₁[pq] ;
H₁(x) c= { F where F is Element of F₂() -tuples_on F₁() : P₁[F] }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H₁(x) or y in { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } )
A7: len pq = F₂() by CARD_1:def 7;
assume y in H₁(x) ; :: thesis: y in { F where F is Element of F₂() -tuples_on F₁() : P₁[F] }
then consider p1, q1 being Element of F₁() * 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) = F₂() by A7, FINSEQ_1:22;
then A10: p1 ^ q1 is Element of F₂() -tuples_on F₁() by FINSEQ_2:92;
P₁[p1 ^ q1] by A6, A9, A1;
hence y in { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } by A10, A8; :: thesis: verum

end;

hence H₁(x) in bool { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } ; :: thesis: verum

end;

consider F being Function of { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } ,(bool { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } ) such that
A11: for x being object st x in { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } holds
F . x = H₁(x) from FUNCT_2:sch 2(A4);
set FF = F ~ ;
A12: dom F = { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } by FUNCT_2:def 1;
A13: F₂() in Seg F₂() by FINSEQ_1:3;
for x being object st x in rng F holds
card (Im ((F ~),x)) = F₂()

proof

let x be object ; :: thesis: ( x in rng F implies card (Im ((F ~),x)) = F₂() )
assume x in rng F ; :: thesis: card (Im ((F ~),x)) = F₂()
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 F₂() -tuples_on F₁() such that
A16: y = p and
A17: P₁[p] by A14, A12;
A18: x = H₁(p) by A14, A15, A16, A11;
defpred S₁[ object , object ] means for i being Nat st i = $1 holds
$2 = (p /^ i) ^ (p | i);
A19: len p = F₂() by CARD_1:def 7;
then ( p /^ F₂() = {} & p | F₂() = p ) by RFINSEQ:27, FINSEQ_1:58;
then A20: p = (p /^ F₂()) ^ (p | F₂()) by FINSEQ_1:34;
A21: for i being object st i in Seg F₂() holds
ex q being object st
( q in Im ((F ~),x) & S₁[i,q] )

proof

let i be object ; :: thesis: ( i in Seg F₂() implies ex q being object st
( q in Im ((F ~),x) & S₁[i,q] ) )
assume i in Seg F₂() ; :: thesis: ex q being object st
( q in Im ((F ~),x) & S₁[i,q] )
then reconsider I = i as Nat ;
set q = p /^ I;
take qp = (p /^ I) ^ (p | I); :: thesis: ( qp in Im ((F ~),x) & S₁[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 = F₂() by FINSEQ_1:22, A19;
then A24: qp is Element of F₂() -tuples_on F₁() by FINSEQ_2:92;
A25: H₁(p) c= H₁(qp)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in H₁(p) or t in H₁(qp) )
assume t in H₁(p) ; :: thesis: t in H₁(qp)
then consider t1, t2 being Element of F₁() * such that
A26: t = t1 ^ t2 and
A27: p = t2 ^ t1 ;
reconsider t12 = t as Element of F₁() * 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 /^ F₂()) ^ (p | F₂()) by A27, A28, A26, FINSEQ_1:33, A20;
then A29: ex k2 being Nat st (t12 /^ k2) ^ (t12 | k2) = p by Th5;
( qp /^ F₂() = {} & qp | F₂() = qp ) by A23, RFINSEQ:27, FINSEQ_1:58;
then (p /^ I) ^ (p | I) = (qp /^ F₂()) ^ (qp | F₂()) 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 F₁() * & t12 | k3 in F₁() * ) by FINSEQ_1:def 11;
then (t12 | k3) ^ (t12 /^ k3) in H₁(qp) by A30;
hence t in H₁(qp) by RFINSEQ:8; :: thesis: verum

end;

P₁[qp] by A1, A17, A22;
then A31: qp in dom F by A24, A12;
then F . qp = H₁(qp) by A11;
then [qp,H₁(qp)] in F by FUNCT_1:def 2, A31;
then A32: [H₁(qp),qp] in F ~ by RELAT_1:def 7;
H₁(qp) c= H₁(p)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in H₁(qp) or t in H₁(p) )
assume t in H₁(qp) ; :: thesis: t in H₁(p)
then consider t1, t2 being Element of F₁() * such that
A33: t = t1 ^ t2 and
A34: (p /^ I) ^ (p | I) = t2 ^ t1 ;
reconsider t12 = t as Element of F₁() * 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 F₁() * & t12 | k in F₁() * ) by FINSEQ_1:def 11;
then (t12 | k) ^ (t12 /^ k) in H₁(p) by A36;
hence t in H₁(p) by RFINSEQ:8; :: thesis: verum

end;

then H₁(qp) = H₁(p) by A25;
hence ( qp in Im ((F ~),x) & S₁[i,qp] ) by A32, RELAT_1:169, A18; :: thesis: verum

end;

consider PR being Function of (Seg F₂()),(Im ((F ~),x)) such that
A37: for i being object st i in Seg F₂() holds
S₁[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 F₂() 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 = H₁(z) by A11;
consider Z being Element of F₂() -tuples_on F₁() such that
A42: z = Z and
P₁[Z] by A40, A12;
A43: ( Z in F₁() * & <*> F₁() in F₁() * ) by FINSEQ_1:def 11;
A44: ( Z = Z ^ (<*> F₁()) & (<*> F₁()) ^ 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 H₁(p) by A44, A43, A41, A42, A18;
then consider z1, z2 being Element of F₁() * 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;

per cases ( len z2 = 0 or len z2 >= 1 ) by NAT_1:14;

suppose len z2 = 0 ; :: thesis: z in rng PR

then A51: p | (len z2) = {} ;
then p /^ (len z2) = p by A49, FINSEQ_1:34;
then z = p by A45, A51, A47, A50, FINSEQ_1:34;
then z = PR . F₂() by A13, A37, A20;
hence z in rng PR by A13, A38, FUNCT_1:def 3; :: thesis: verum

end;

suppose len z2 >= 1 ; :: thesis: z in rng PR

then A52: len z2 in Seg F₂() by A19, A48;
then PR . (len z2) = z by A47, A50, A45, A37;
hence z in rng PR by A52, A38, FUNCT_1:def 3; :: thesis: verum

end;

end;

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 <= F₂() 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 F₁() * by FINSEQ_1:def 11;
A61: i1 <= F₂() by A54, FINSEQ_1:1;
A62: F₂() - 1 < F₂() - 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 <= F₂() - 1 by A57, A59, XREAL_1:13;
then i2 - i1 < F₂() 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 <= F₂() - 1 by A61, A58, XREAL_1:13;
then i1 - i2 < F₂() 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 F₂()) by A53, A38, WELLORD2:def 4, CARD_1:5
.= F₂() by FINSEQ_1:57 ;
:: thesis: verum

end;

then A65: card (F ~) = (card ((F ~) | ((dom (F ~)) \ (rng F)))) +` (F<sub>2</sub>() *` (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 F₂() *` (card (rng F)) = card (F ~) by A65, CARD_2:18
.= card F by Th1
.= card { F where F is Element of F<sub>2</sub>() -tuples_on F<sub>1</sub>() : P<sub>1</sub>[F] } by A12, CARD_1:62 ;
hence ex C being Cardinal st F<sub>2</sub>() *` C = card { F where F is Element of F₂() -tuples_on F₁() : P₁[F] } ; :: thesis: verum

end;

end;