let p be FinSequence; :: thesis: for x being object
for n being Nat st x in rng p & n = (len p) - (x .. p) holds
dom (p |-- x) = Seg n
let x be object ; :: thesis: for n being Nat st x in rng p & n = (len p) - (x .. p) holds
dom (p |-- x) = Seg n
let n be Nat; :: thesis: ( x in rng p & n = (len p) - (x .. p) implies dom (p |-- x) = Seg n )
assume x in rng p ; :: thesis: ( not n = (len p) - (x .. p) or dom (p |-- x) = Seg n )
then len (p |-- x) = (len p) - (x .. p) by Def6;
hence ( not n = (len p) - (x .. p) or dom (p |-- x) = Seg n ) by FINSEQ_1:def 3; :: thesis: verum