defpred S₁[ set ] means ex s being one-to-one FinSequence st
( rng s = $1 & ( for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j ) );
A3: S₁[ {} ]

proof

reconsider s = {} as one-to-one FinSequence ;
take s ; :: thesis: ( rng s = {} & ( for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j ) )
thus ( rng s = {} & ( for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j ) ) ; :: thesis: verum

end;

A4: for A being Subset of F₁() st ( for B being set st B c< A holds
S₁[B] ) holds
S₁[A]

proof

let A be Subset of F₁(); :: thesis: ( ( for B being set st B c< A holds
S₁[B] ) implies S₁[A] )
assume A5: for B being set st B c< A holds
S₁[B] ; :: thesis: S₁[A]

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: S₁[A]

hence S₁[A] by A3; :: thesis: verum

end;

suppose not A is empty ; :: thesis: S₁[A]

then reconsider A9 = A as non empty finite set ;
A6: for x, y being set st x in A9 & y in A9 & P₁[x,y] holds
not P₁[y,x] by A1;
A7: for x, y, z being set st x in A9 & y in A9 & z in A9 & P₁[x,y] & P₁[y,z] holds
P₁[x,z] by A2;
consider x being set such that
A8: ( x in A9 & ( for y being set st y in A9 holds
not P₁[y,x] ) ) from ABCMIZ_A:sch 1(A6, A7);
set B = A \ {x};
A9: ( x nin A \ {x} & A \ {x} c= A ) by ZFMISC_1:56;
then A \ {x} c< A by A8;
then consider s being one-to-one FinSequence such that
A10: rng s = A \ {x} and
A11: for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j by A5;
( <*x*> is one-to-one & rng <*x*> = {x} & {x} misses A \ {x} ) by FINSEQ_1:39, FINSEQ_3:93, XBOOLE_1:79;
then reconsider s9 = <*x*> ^ s as one-to-one FinSequence by A10, FINSEQ_3:91;
A12: {x} c= A by A8, ZFMISC_1:31;
A13: len <*x*> = 1 by FINSEQ_1:40;
thus S₁[A] :: thesis: verum

proof

take s9 ; :: thesis: ( rng s9 = A & ( for i, j being Nat st i in dom s9 & j in dom s9 & P₁[s9 . i,s9 . j] holds
i < j ) )
thus rng s9 = (rng <*x*>) \/ (rng s) by FINSEQ_1:31
.= {x} \/ (A \ {x}) by A10, FINSEQ_1:38
.= A by A12, XBOOLE_1:45 ; :: thesis: for i, j being Nat st i in dom s9 & j in dom s9 & P₁[s9 . i,s9 . j] holds
i < j
let i, j be Nat; :: thesis: ( i in dom s9 & j in dom s9 & P₁[s9 . i,s9 . j] implies i < j )
assume A14: ( i in dom s9 & j in dom s9 & P₁[s9 . i,s9 . j] ) ; :: thesis: i < j
A15: dom <*x*> = Seg 1 by FINSEQ_1:38;

per cases ( ( i in dom <*x*> & j in dom <*x*> ) or ( i in dom <*x*> & ex n being Nat st
( n in dom s & j = 1 + n ) ) or ( j in dom <*x*> & ex n being Nat st
( n in dom s & i = 1 + n ) ) or ( ex n being Nat st
( n in dom s & i = 1 + n ) & ex n being Nat st
( n in dom s & j = 1 + n ) ) ) by A13, A14, FINSEQ_1:25;

suppose ( i in dom <*x*> & j in dom <*x*> ) ; :: thesis: i < j

then ( i = 1 & j = 1 ) by A15, FINSEQ_1:2, TARSKI:def 1;
then ( s9 . i = x & s9 . j = x ) by FINSEQ_1:41;
hence i < j by A8, A14; :: thesis: verum

end;

suppose A16: ( i in dom <*x*> & ex n being Nat st
( n in dom s & j = 1 + n ) ) ; :: thesis: i < j

then A17: i = 1 by A15, FINSEQ_1:2, TARSKI:def 1;
consider n being Nat such that
A18: ( n in dom s & j = 1 + n ) by A16;
1 <= n by A18, FINSEQ_3:25;
hence i < j by A17, A18, NAT_1:13; :: thesis: verum

end;

suppose A19: ( j in dom <*x*> & ex n being Nat st
( n in dom s & i = 1 + n ) ) ; :: thesis: i < j

then j = 1 by A15, FINSEQ_1:2, TARSKI:def 1;
then A20: s9 . j = x by FINSEQ_1:41;
consider n being Nat such that
A21: ( n in dom s & i = 1 + n ) by A19;
s9 . i = s . n by A13, A21, FINSEQ_1:def 7;
then s9 . i in rng s by A21, FUNCT_1:def 3;
hence i < j by A8, A14, A20, A9, A10; :: thesis: verum

end;

suppose ( ex n being Nat st
( n in dom s & i = 1 + n ) & ex n being Nat st
( n in dom s & j = 1 + n ) ) ; :: thesis: i < j

then consider ni, nj being Nat such that
A22: ( ni in dom s & i = 1 + ni & nj in dom s & j = 1 + nj ) ;
( s9 . i = s . ni & s9 . j = s . nj ) by A13, A22, FINSEQ_1:def 7;
then ni < nj by A11, A14, A22;
hence i < j by A22, XREAL_1:6; :: thesis: verum

end;

end;

end;

end;

end;

end;

thus S₁[F₁()] from ABCMIZ_A:sch 2(A4); :: thesis: verum