defpred S1[ Element of NAT , set , set ] means c3 = [(choose (c2 `2 )),((c2 `2 ) \ {(choose (c2 `2 ))})];
set cA = card A;
A1: for n being Element of NAT st 1 <= n & n < card A holds
for x being set ex y being set st S1[n,x,y] ;
consider f being FinSequence such that
A2: len f = card A and
A3: ( f . 1 = [(choose A),(A \ {(choose A)})] or card A = 0 ) and
A4: for n being Element of NAT st 1 <= n & n < card A holds
S1[n,f . n,f . (n + 1)] from RECDEF_1:sch 3(A1);
 defpred S2[ Element of NAT ] means ( A in dom f implies ( f . A in [:A,(bool A):] & ex X being finite set st
( X = (f . A) `2 & (card X) + A = card A ) ) );
A5: for i being Element of NAT st 1 <= i & i < len f & S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f & S2[i] implies S2[i + 1] )
assume that
A6: 1 <= i and
A7: i < len f and
A8: S2[i] and
i + 1 in dom f ; :: thesis: ( f . (i + 1) in [:A,(bool A):] & ex X being finite set st
( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A ) )
A9: f . (i + 1) = [(choose ((f . i) `2 )),(((f . i) `2 ) \ {(choose ((f . i) `2 ))})] by A2, A4, A6, A7;
consider a, ba being set such that
a in A and
A10: ba in bool A and
A11: f . i = [a,ba] by A6, A7, A8, FINSEQ_3:27, ZFMISC_1:def 2;
A12: (f . i) `2 = ba by A11, MCART_1:7;
then A13: ((f . i) `2 ) \ {(choose ((f . i) `2 ))} c= A by A10, XBOOLE_1:1;
A14: now
assume choose ((f . i) `2 ) in ((f . i) `2 ) \ {(choose ((f . i) `2 ))} ; :: thesis: contradiction
then not choose ((f . i) `2 ) in {(choose ((f . i) `2 ))} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
consider X being finite set such that
A15: X = (f . i) `2 and
A16: (card X) + i = card A by A6, A7, A8, FINSEQ_3:27;
A17: X <> {} by A2, A7, A16, CARD_1:47;
then choose ((f . i) `2 ) in (f . i) `2 by A15;
hence f . (i + 1) in [:A,(bool A):] by A10, A9, A12, A13, ZFMISC_1:def 2; :: thesis: ex X being finite set st
( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A )
reconsider XX = ((f . i) `2 ) \ {(choose ((f . i) `2 ))} as finite set by A15;
take XX ; :: thesis: ( XX = (f . (i + 1)) `2 & (card XX) + (i + 1) = card A )
thus XX = (f . (i + 1)) `2 by A9, MCART_1:7; :: thesis: (card XX) + (i + 1) = card A
{(choose ((f . i) `2 ))} c= (f . i) `2 by A15, A17, ZFMISC_1:37;
then (f . i) `2 = {(choose ((f . i) `2 ))} \/ (((f . i) `2 ) \ {(choose ((f . i) `2 ))}) by XBOOLE_1:45;
then card X = (card XX) + 1 by A15, A14, CARD_2:54;
hence (card XX) + (i + 1) = card A by A16; :: thesis: verum
end;
A18: S2[1]
proof
reconsider X = A \ {(choose A)} as finite set ;
A19: now
assume choose A in A \ {(choose A)} ; :: thesis: contradiction
then not choose A in {(choose A)} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
assume A20: 1 in dom f ; :: thesis: ( f . 1 in [:A,(bool A):] & ex X being finite set st
( X = (f . 1) `2 & (card X) + 1 = card A ) )
then A <> {} by A2, FINSEQ_3:27;
hence f . 1 in [:A,(bool A):] by A3, ZFMISC_1:def 2; :: thesis: ex X being finite set st
( X = (f . 1) `2 & (card X) + 1 = card A )
take X ; :: thesis: ( X = (f . 1) `2 & (card X) + 1 = card A )
thus X = (f . 1) `2 by A2, A3, A20, FINSEQ_3:27, MCART_1:7; :: thesis: (card X) + 1 = card A
0 + 1 <= len f by A20, FINSEQ_3:27;
then {(choose A)} c= A by A2, CARD_1:47, ZFMISC_1:37;
then A = {(choose A)} \/ (A \ {(choose A)}) by XBOOLE_1:45;
hence (card X) + 1 = card A by A19, CARD_2:54; :: thesis: verum
end;
A21: for i being Element of NAT st 1 <= i & i <= len f holds
S2[i] from UPROOTS:sch 1(A18, A5);
 rng f c= [:A,(bool A):]
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in [:A,(bool A):] )
assume y in rng f ; :: thesis: y in [:A,(bool A):]
then consider i being Nat such that
A22: i in dom f and
A23: y = f . i by FINSEQ_2:11;
( 1 <= i & i <= len f ) by A22, FINSEQ_3:27;
hence y in [:A,(bool A):] by A21, A22, A23; :: thesis: verum
end;
then reconsider f = f as FinSequence of [:A,(bool A):] by FINSEQ_1:def 4;
deffunc H1( Nat) -> set = (f . A) `1 ;
consider p being FinSequence such that
A24: len p = card A and
A25: for k being Nat st k in dom p holds
p . k = H1(k) from FINSEQ_1:sch 2();
 A26: dom p = dom f by A2, A24, FINSEQ_3:31;
rng p c= A
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in A )
assume y in rng p ; :: thesis: y in A
then consider i being Nat such that
A27: i in dom p and
A28: p . i = y by FINSEQ_2:11;
( p . i = (f . i) `1 & f . i in [:A,(bool A):] ) by A25, A26, A27, FINSEQ_2:13;
hence y in A by A28, MCART_1:10; :: thesis: verum
end;
then reconsider p = p as FinSequence of A by FINSEQ_1:def 4;
A29: rng p = A
proof
set F = p;
per cases ( A = {} or A <> {} ) ;
suppose A = {} ; :: thesis: rng p = A
hence rng p = A ; :: thesis: verum
end;
suppose A30: A <> {} ; :: thesis: rng p = A
defpred S3[ Element of NAT ] means ( (rng (p | (Seg A))) \/ ((f . A) `2 ) = A & ex X being finite set st
( X = (f . A) `2 & (card X) + A = card A ) );
A31: for i being Element of NAT st 1 <= i & i < len f & S3[i] holds
S3[i + 1]
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f & S3[i] implies S3[i + 1] )
assume that
A32: 1 <= i and
A33: i < len f and
A34: S3[i] ; :: thesis: S3[i + 1]
A35: f . (i + 1) = [(choose ((f . i) `2 )),(((f . i) `2 ) \ {(choose ((f . i) `2 ))})] by A2, A4, A32, A33;
consider X being finite set such that
A36: X = (f . i) `2 and
A37: (card X) + i = card A by A34;
reconsider XX = ((f . i) `2 ) \ {(choose ((f . i) `2 ))} as finite set by A36;
not (f . i) `2 is empty by A2, A33, A36, A37, CARD_1:47;
then {(choose ((f . i) `2 ))} c= (f . i) `2 by ZFMISC_1:37;
then A38: (f . i) `2 = {(choose ((f . i) `2 ))} \/ (((f . i) `2 ) \ {(choose ((f . i) `2 ))}) by XBOOLE_1:45;
reconsider Fi = p | (Seg i), Fi1 = p | (Seg (i + 1)) as FinSequence of A by FINSEQ_1:23;
A39: i + 1 <= len p by A2, A24, A33, NAT_1:13;
then consider a being Element of A such that
A40: Fi1 = Fi ^ <*a*> by A30, QC_LANG4:6;
1 <= i + 1 by NAT_1:12;
then A41: i + 1 in dom p by A39, FINSEQ_3:27;
A42: rng Fi1 = (rng Fi) \/ (rng <*a*>) by A40, FINSEQ_1:44
.= (rng Fi) \/ {a} by FINSEQ_1:56 ;
( p . (i + 1) = Fi1 . (i + 1) & i = len Fi ) by A2, A24, A33, FINSEQ_1:6, FINSEQ_1:21, FUNCT_1:72;
then A43: a = p . (i + 1) by A40, FINSEQ_1:59
.= (f . (i + 1)) `1 by A25, A41
.= choose ((f . i) `2 ) by A35, MCART_1:7 ;
then (f . (i + 1)) `2 = ((f . i) `2 ) \ {a} by A35, MCART_1:7;
hence (rng (p | (Seg (i + 1)))) \/ ((f . (i + 1)) `2 ) = A by A34, A38, A42, A43, XBOOLE_1:4; :: thesis: ex X being finite set st
( X = (f . (i + 1)) `2 & (card X) + (i + 1) = card A )
take XX ; :: thesis: ( XX = (f . (i + 1)) `2 & (card XX) + (i + 1) = card A )
thus XX = (f . (i + 1)) `2 by A35, MCART_1:7; :: thesis: (card XX) + (i + 1) = card A
now
assume choose ((f . i) `2 ) in ((f . i) `2 ) \ {(choose ((f . i) `2 ))} ; :: thesis: contradiction
then not choose ((f . i) `2 ) in {(choose ((f . i) `2 ))} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
then card X = (card XX) + 1 by A36, A38, CARD_2:54;
hence (card XX) + (i + 1) = card A by A37; :: thesis: verum
end;
A44: 0 + 1 <= len p by A24, A30, NAT_1:13;
then A45: 1 in dom p by FINSEQ_3:27;
A46: S3[1]
proof
reconsider X = A \ {(choose A)} as finite set ;
reconsider F1 = p | (Seg 1) as FinSequence of A by FINSEQ_1:23;
1 in Seg (0 + 1) by FINSEQ_1:6;
then A48: F1 . 1 = p . 1 by FUNCT_1:72
.= (f . 1) `1 by A25, A45
.= choose A by A3, A30, MCART_1:7 ;
ex a being Element of A st F1 = <*a*> by A30, A44, QC_LANG4:7;
then p | (Seg 1) = <*(choose A)*> by A48, FINSEQ_1:57;
then A49: rng (p | (Seg 1)) = {(choose A)} by FINSEQ_1:56;
(f . 1) `2 = A \ {(choose A)} by A3, A30, MCART_1:7;
hence (rng (p | (Seg 1))) \/ ((f . 1) `2 ) = A by A49, XBOOLE_1:45; :: thesis: ex X being finite set st
( X = (f . 1) `2 & (card X) + 1 = card A )
take X ; :: thesis: ( X = (f . 1) `2 & (card X) + 1 = card A )
thus X = (f . 1) `2 by A3, A30, MCART_1:7; :: thesis: (card X) + 1 = card A
{(choose A)} c= A by A30, ZFMISC_1:37;
then A = {(choose A)} \/ (A \ {(choose A)}) by XBOOLE_1:45;
hence (card X) + 1 = card A by A47, CARD_2:54; :: thesis: verum
end;
A50: for i being Element of NAT st 1 <= i & i <= len f holds
S3[i] from UPROOTS:sch 1(A46, A31);
A51: len p >= 1 by A24, A30, NAT_1:14;
then consider X being finite set such that
A52: X = (f . (len p)) `2 and
A53: (card X) + (len f) = card A by A2, A24, A50;
p = p | (Seg (len p)) by FINSEQ_3:55;
then A54: (rng p) \/ ((f . (len p)) `2 ) = A by A2, A24, A50, A51;
X = {} by A2, A53;
hence rng p = A by A54, A52; :: thesis: verum
end;
end;
end;
then A55: p is onto by FUNCT_2:def 3;
take p ; :: thesis: p is bijective
p is one-to-one by A24, A29, FINSEQ_4:77;
hence p is bijective by A55; :: thesis: verum