let p be FinSequence; :: thesis: ( rng p c= dom p & p is one-to-one implies rng p = dom p )
defpred S₁[ Nat] means for q being FinSequence st len q = $1 & rng q c= dom q & q is one-to-one holds
rng q = dom q;
A1: len p = len p ;

now :: thesis: for k being Nat st ( for q being FinSequence st len q = k & rng q c= dom q & q is one-to-one holds
rng q = dom q ) holds
for q being FinSequence st len q = k + 1 & rng q c= dom q & q is one-to-one holds
rng q = dom q

let k be Nat; :: thesis: ( ( for q being FinSequence st len q = k & rng q c= dom q & q is one-to-one holds
rng q = dom q ) implies for q being FinSequence st len q = k + 1 & rng q c= dom q & q is one-to-one holds
rng q = dom q )
assume A2: for q being FinSequence st len q = k & rng q c= dom q & q is one-to-one holds
rng q = dom q ; :: thesis: for q being FinSequence st len q = k + 1 & rng q c= dom q & q is one-to-one holds
rng q = dom q
let q be FinSequence; :: thesis: ( len q = k + 1 & rng q c= dom q & q is one-to-one implies rng q = dom q )
assume that
A3: len q = k + 1 and
A4: rng q c= dom q and
A5: q is one-to-one ; :: thesis: rng q = dom q
A6: dom q = Seg (k + 1) by A3, FINSEQ_1:def 3;
dom q c= rng q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom q or x in rng q )
assume A7: x in dom q ; :: thesis: x in rng q
then reconsider n = x as Element of NAT ;

per cases ( k + 1 in rng q or not k + 1 in rng q ) ;

suppose A8: k + 1 in rng q ; :: thesis: x in rng q

now :: thesis: x in rng q

per cases ( n = k + 1 or n <> k + 1 ) ;

suppose n = k + 1 ; :: thesis: x in rng q

hence x in rng q by A8; :: thesis: verum

end;

suppose n <> k + 1 ; :: thesis: x in rng q

then not x in {(k + 1)} by TARSKI:def 1;
then x in (Seg (k + 1)) \ {(k + 1)} by A6, A7, XBOOLE_0:def 5;
then A9: x in Seg k by FINSEQ_1:10;
set r = q - {(k + 1)};
A10: len (q - {(k + 1)}) = (k + 1) - 1 by A3, A5, A8, FINSEQ_3:90;
then A11: dom (q - {(k + 1)}) = Seg k by FINSEQ_1:def 3;
A12: rng (q - {(k + 1)}) = (rng q) \ {(k + 1)} by FINSEQ_3:65;
then rng (q - {(k + 1)}) c= (Seg (k + 1)) \ {(k + 1)} by A4, A6, XBOOLE_1:33;
then rng (q - {(k + 1)}) c= dom (q - {(k + 1)}) by A11, FINSEQ_1:10;
then rng (q - {(k + 1)}) = dom (q - {(k + 1)}) by A2, A5, A10, FINSEQ_3:87;
hence x in rng q by A12, A11, A9; :: thesis: verum

end;

end;

end;

hence x in rng q ; :: thesis: verum

end;

suppose A13: not k + 1 in rng q ; :: thesis: x in rng q

A14: rng q c= Seg k

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in Seg k )
assume A15: x in rng q ; :: thesis: x in Seg k
then not x in {(k + 1)} by A13, TARSKI:def 1;
then x in (Seg (k + 1)) \ {(k + 1)} by A4, A6, A15, XBOOLE_0:def 5;
hence x in Seg k by FINSEQ_1:10; :: thesis: verum

end;

A16: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A17: q . (k + 1) in rng q by A6, FUNCT_1:def 3;
reconsider r = q | (Seg k) as FinSequence by FINSEQ_1:15;
A18: ( dom r c= dom q & k < k + 1 ) by RELAT_1:60, XREAL_1:29;
A19: len r = k by A3, FINSEQ_3:53;
then A20: dom r = Seg k by FINSEQ_1:def 3;
( rng r c= rng q & r is one-to-one ) by A5, FUNCT_1:52, RELAT_1:70;
then rng r = dom r by A2, A19, A20, A14, XBOOLE_1:1;
then consider x being object such that
A21: x in dom r and
A22: r . x = q . (k + 1) by A20, A14, A17, FUNCT_1:def 3;
reconsider n = x as Element of NAT by A21;
( r . x = q . x & n <= k ) by A20, A21, FINSEQ_1:1, FUNCT_1:49;
hence x in rng q by A5, A6, A16, A21, A22, A18; :: thesis: verum

end;

end;

end;

hence rng q = dom q by A4; :: thesis: verum

end;

then A23: for k being Nat st S₁[k] holds
S₁[k + 1] ;

now :: thesis: for q being FinSequence st len q = 0 & rng q c= dom q & q is one-to-one holds
rng q = dom q

let q be FinSequence; :: thesis: ( len q = 0 & rng q c= dom q & q is one-to-one implies rng q = dom q )
assume A24: len q = 0 ; :: thesis: ( rng q c= dom q & q is one-to-one implies rng q = dom q )
assume that
rng q c= dom q and
q is one-to-one ; :: thesis: rng q = dom q
q = {} by A24;
hence rng q = dom q ; :: thesis: verum

end;

then A25: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A25, A23);
hence ( rng p c= dom p & p is one-to-one implies rng p = dom p ) by A1; :: thesis: verum