assume A3: 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] ) );
A4: for m being 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 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 A5: x nin F1() ; :: thesis: ex y being set st S1[m,x,y]
set y = the set ;
take the set ; :: thesis: S1[m,x, the set ]
thus S1[m,x, the set ] by A5; :: thesis: verum
end;
suppose x in F1() ; :: thesis: ex y being set st S1[m,x,y]
then consider y being set such that
A6: ( y in F1() & P1[y,x] ) by A3;
take y ; :: thesis: S1[m,x,y]
thus S1[m,x,y] by A6; :: thesis: verum
end;
end;
end;
consider p being FinSequence such that
A7: len p = (card F1()) + 1 and
A8: ( p . 1 = the Element of F1() or (card F1()) + 1 = 0 ) and
A9: for i being Nat st 1 <= i & i < (card F1()) + 1 holds
S1[i,p . i,p . (i + 1)] from RECDEF_1:sch 3(A4);
 defpred S2[ Nat] means ( $1 in dom p implies p . $1 in F1() );
A10: S2[ 0 ] by FINSEQ_3:25;
A11: now :: thesis: for i being Nat st S2[i] holds
S2[i + 1]
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A12: 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 A7, FINSEQ_3:25;
then A13: i < (card F1()) + 1 by NAT_1:13;
per cases ( i = 0 or i > 0 ) ;
suppose i = 0 ; :: thesis: p . (i + 1) in F1()
hence p . (i + 1) in F1() by A8; :: 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 12;
hence p . (i + 1) in F1() by A12, A7, A9, A13, FINSEQ_3:25; :: thesis: verum
end;
end;
end;
end;
A14: for i being Nat holds S2[i] from NAT_1:sch 2(A10, A11);
 A15: rng p c= F1()
proof
let x be object ; :: 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 object st
( i in dom p & x = p . i ) by FUNCT_1:def 3;
hence x in F1() by A14; :: thesis: verum
end;
A16: 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 A17: 1 <= i ; :: thesis: ( not i < j or not j <= (card F1()) + 1 or P1[p . j,p . i] )
assume A18: 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
A19: j = (i + 1) + k by NAT_1:10;
assume A20: j <= (card F1()) + 1 ; :: thesis: P1[p . j,p . i]
then i <= (card F1()) + 1 by A18, XXREAL_0:2;
then A21: i in dom p by A17, A7, FINSEQ_3:25;
defpred S3[ Nat] means ( (i + 1) + $1 <= (card F1()) + 1 implies P1[p . ((i + 1) + $1),p . i] );
A22: S3[ 0 ]
proof
assume (i + 1) + 0 <= (card F1()) + 1 ; :: thesis: P1[p . ((i + 1) + 0),p . i]
then A23: i < (card F1()) + 1 by NAT_1:13;
( p . i in F1() & i is Element of NAT ) by A14, A21;
hence P1[p . ((i + 1) + 0),p . i] by A9, A17, A23; :: thesis: verum
end;
A24: now :: thesis: for k being Nat st S3[k] holds
S3[k + 1]
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A25: S3[k] ; :: thesis: S3[k + 1]
thus S3[k + 1] :: thesis: verum
proof
assume A26: (i + 1) + (k + 1) <= (card F1()) + 1 ; :: thesis: P1[p . ((i + 1) + (k + 1)),p . i]
A27: (i + 1) + (k + 1) = ((i + 1) + k) + 1 ;
then A28: (i + 1) + k < (card F1()) + 1 by A26, NAT_1:13;
A29: p . i in F1() by A14, A21;
(i + 1) + k = 1 + (i + k) ;
then A30: 1 <= (i + 1) + k by NAT_1:11;
then (i + 1) + k in dom p by A7, A28, FINSEQ_3:25;
then A31: ( p . ((i + 1) + k) in F1() & (i + 1) + k is Element of NAT ) by A14;
then ( p . ((i + 1) + (k + 1)) in F1() & P1[p . ((i + 1) + (k + 1)),p . ((i + 1) + k)] ) by A9, A28, A27, A30;
hence P1[p . ((i + 1) + (k + 1)),p . i] by A2, A28, A25, A31, A29; :: thesis: verum
end;
end;
for k being Nat holds S3[k] from NAT_1:sch 2(A22, A24);
 hence P1[p . j,p . i] by A19, A20; :: thesis: verum
end;
A32: ( dom p = Seg ((card F1()) + 1) & card (Seg ((card F1()) + 1)) = (card F1()) + 1 ) by A7, FINSEQ_1:57, FINSEQ_1:def 3;
Segm (card (rng p)) c= Segm (card F1()) by A15, CARD_1:11;
then ( card (rng p) <= card F1() & card F1() < (card F1()) + 1 ) by NAT_1:19, NAT_1:39;
then not dom p, rng p are_equipotent by A32, CARD_1:5;
then not p is one-to-one by WELLORD2:def 4;
then consider i, j being object such that
A33: ( i in dom p & j in dom p & p . i = p . j & i <> j ) ;
reconsider i = i, j = j as Nat by A33;
A34: ( 1 <= i & 1 <= j & i <= (card F1()) + 1 & j <= (card F1()) + 1 ) by A7, A33, FINSEQ_3:25;
p . i in rng p by A33, FUNCT_1:def 3;
then A35: p . i in F1() by A15;
( i < j or j < i ) by A33, XXREAL_0:1;
then P1[p . i,p . i] by A16, A33, A34;
hence contradiction by A1, A35; :: thesis: verum