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;

now

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

end;

then A2: S₁[ 0 ] ;

now

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 A3: 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
A4: len q = k + 1 and
A5: rng q c= dom q and
A6: q is one-to-one ; :: thesis: rng q = dom q
A7: dom q = Seg (k + 1) by A4, FINSEQ_1:def 3;
dom q c= rng q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom q or x in rng q )
assume A8: 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 A9: k + 1 in rng q ; :: thesis: x in rng q

now

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

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

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

end;

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

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

end;

end;

end;

hence x in rng q ; :: thesis: verum

end;

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

reconsider r = q | (Seg k) as FinSequence by FINSEQ_1:19;
A16: len r = k by A4, FINSEQ_3:59;
then A17: ( dom r = Seg k & rng r c= rng q ) by FINSEQ_1:def 3, RELAT_1:99;
A18: rng q c= Seg k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in Seg k )
assume x in rng q ; :: thesis: x in Seg k
then ( x in Seg (k + 1) & not x in {(k + 1)} ) by A5, A7, A15, TARSKI:def 1;
then x in (Seg (k + 1)) \ {(k + 1)} by XBOOLE_0:def 5;
hence x in Seg k by FINSEQ_1:12; :: thesis: verum

end;

r is one-to-one by A6, FUNCT_1:84;
then A19: rng r = dom r by A3, A16, A17, A18, XBOOLE_1:1;
A20: k + 1 in Seg (k + 1) by FINSEQ_1:6;
then q . (k + 1) in rng q by A7, FUNCT_1:def 5;
then consider x being set such that
A21: x in dom r and
A22: r . x = q . (k + 1) by A17, A18, A19, FUNCT_1:def 5;
reconsider n = x as Element of NAT by A21;
A23: dom r c= dom q by RELAT_1:89;
A24: r . x = q . x by A17, A21, FUNCT_1:72;
( n <= k & k < k + 1 ) by A17, A21, FINSEQ_1:3, XREAL_1:31;
hence x in rng q by A6, A7, A20, A21, A22, A23, A24, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence rng q = dom q by A5, XBOOLE_0:def 10; :: thesis: verum

end;

then A25: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A26: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A25);
len p = len p ;
hence ( rng p c= dom p & p is one-to-one implies rng p = dom p ) by A26; :: thesis: verum