assume A0: for x being set st x in F1() holds
ex y being set st
( y in F1() & P1[y,x] ) ; :: thesis: contradiction
set n = card F1();
set x0 = the Element of F1();
defpred S1[ Nat, set , set ] means ( $2 in F1() implies ( $3 in F1() & P1[$3,$2] ) );
B0: for m being Element of NAT st 1 <= m & m < (card F1()) + 1 holds
for x being set ex y being set st S1[m,x,y]
proof
let m be Element of NAT ; :: thesis: ( 1 <= m & m < (card F1()) + 1 implies for x being set ex y being set st S1[m,x,y] )
assume ( 1 <= m & m < (card F1()) + 1 ) ; :: thesis: for x being set ex y being set st S1[m,x,y]
let x be set ; :: thesis: ex y being set st S1[m,x,y]
per cases ( x nin F1() or x in F1() ) ;
suppose Z1: x nin F1() ; :: thesis: ex y being set st S1[m,x,y]
consider y being set ;
take y ; :: thesis: S1[m,x,y]
thus S1[m,x,y] by Z1; :: thesis: verum
end;
suppose x in F1() ; :: thesis: ex y being set st S1[m,x,y]
then consider y being set such that
Z2: ( y in F1() & P1[y,x] ) by A0;
take y ; :: thesis: S1[m,x,y]
thus S1[m,x,y] by Z2; :: thesis: verum
end;
end;
end;
consider p being FinSequence such that
B1: len p = (card F1()) + 1 and
BB: ( p . 1 = the Element of F1() or (card F1()) + 1 = 0 ) and
B2: for i being Element of NAT st 1 <= i & i < (card F1()) + 1 holds
S1[i,p . i,p . (i + 1)] from RECDEF_1:sch 3(B0);
 defpred S2[ Nat] means ( $1 in dom p implies p . $1 in F1() );
S0: S2[ 0 ] by FINSEQ_3:27;
S1: now
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume S2: S2[i] ; :: thesis: S2[i + 1]
thus S2[i + 1] :: thesis: verum
proof
assume i + 1 in dom p ; :: thesis: p . (i + 1) in F1()
then i + 1 <= (card F1()) + 1 by B1, FINSEQ_3:27;
then S4: i < (card F1()) + 1 by NAT_1:13;
per cases ( i = 0 or i > 0 ) by NAT_1:3;
suppose i = 0 ; :: thesis: p . (i + 1) in F1()
hence p . (i + 1) in F1() by BB; :: thesis: verum
end;
suppose i > 0 ; :: thesis: p . (i + 1) in F1()
then ( i >= 0 + 1 & i is Element of NAT ) by NAT_1:13, ORDINAL1:def 13;
hence p . (i + 1) in F1() by S2, B1, B2, S4, FINSEQ_3:27; :: thesis: verum
end;
end;
end;
end;
SK: for i being Nat holds S2[i] from NAT_1:sch 2(S0, S1);
 C0: rng p c= F1()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in F1() )
assume x in rng p ; :: thesis: x in F1()
then ex i being set st
( i in dom p & x = p . i ) by FUNCT_1:def 5;
hence x in F1() by SK; :: thesis: verum
end;
CC: for i, j being Nat st 1 <= i & i < j & j <= (card F1()) + 1 holds
P1[p . j,p . i]
proof
let i, j be Nat; :: thesis: ( 1 <= i & i < j & j <= (card F1()) + 1 implies P1[p . j,p . i] )
assume Z0: 1 <= i ; :: thesis: ( not i < j or not j <= (card F1()) + 1 or P1[p . j,p . i] )
assume Z3: i < j ; :: thesis: ( not j <= (card F1()) + 1 or P1[p . j,p . i] )
then i + 1 <= j by NAT_1:13;
then consider k being Nat such that
Z1: j = (i + 1) + k by NAT_1:10;
assume Z2: j <= (card F1()) + 1 ; :: thesis: P1[p . j,p . i]
then i <= (card F1()) + 1 by Z3, XXREAL_0:2;
then Z4: i in dom p by Z0, B1, FINSEQ_3:27;
defpred S3[ Nat] means ( (i + 1) + $1 <= (card F1()) + 1 implies P1[p . ((i + 1) + $1),p . i] );
R0: S3[ 0 ]
proof
assume (i + 1) + 0 <= (card F1()) + 1 ; :: thesis: P1[p . ((i + 1) + 0 ),p . i]
then G1: i < (card F1()) + 1 by NAT_1:13;
( p . i in F1() & i is Element of NAT ) by SK, Z4;
hence P1[p . ((i + 1) + 0 ),p . i] by B2, Z0, G1; :: thesis: verum
end;
R1: now
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume G2: S3[k] ; :: thesis: S3[k + 1]
thus S3[k + 1] :: thesis: verum
proof
assume G0: (i + 1) + (k + 1) <= (card F1()) + 1 ; :: thesis: P1[p . ((i + 1) + (k + 1)),p . i]
G4: (i + 1) + (k + 1) = ((i + 1) + k) + 1 ;
then G1: (i + 1) + k < (card F1()) + 1 by G0, NAT_1:13;
G7: p . i in F1() by SK, Z4;
(i + 1) + k = 1 + (i + k) ;
then G5: 1 <= (i + 1) + k by NAT_1:11;
then (i + 1) + k in dom p by B1, G1, FINSEQ_3:27;
then G6: ( p . ((i + 1) + k) in F1() & (i + 1) + k is Element of NAT ) by SK;
then ( p . ((i + 1) + (k + 1)) in F1() & P1[p . ((i + 1) + (k + 1)),p . ((i + 1) + k)] ) by B2, G1, G4, G5;
hence P1[p . ((i + 1) + (k + 1)),p . i] by P2, G1, G2, G6, G7; :: thesis: verum
end;
end;
for k being Nat holds S3[k] from NAT_1:sch 2(R0, R1);
 hence P1[p . j,p . i] by Z1, Z2; :: thesis: verum
end;
B3: ( dom p = Seg ((card F1()) + 1) & card (Seg ((card F1()) + 1)) = (card F1()) + 1 ) by B1, FINSEQ_1:def 3, FINSEQ_1:78;
card (rng p) c= card F1() by C0, CARD_1:27;
then ( card (rng p) <= card F1() & card F1() < (card F1()) + 1 ) by NAT_1:19, NAT_1:40;
then not dom p, rng p are_equipotent by CARD_1:21, B3;
then not p is one-to-one by WELLORD2:def 4;
then consider i, j being set such that
D1: ( i in dom p & j in dom p & p . i = p . j & i <> j ) by FUNCT_1:def 8;
reconsider i = i, j = j as Nat by D1;
D2: ( 1 <= i & 1 <= j & i <= (card F1()) + 1 & j <= (card F1()) + 1 ) by B1, D1, FINSEQ_3:27;
p . i in rng p by D1, FUNCT_1:def 5;
then D3: p . i in F1() by C0;
( i < j or j < i ) by D1, XXREAL_0:1;
then P1[p . i,p . i] by CC, D1, D2;
hence contradiction by P1, D3; :: thesis: verum