let p be FinSequence; :: thesis: for x being object st x in rng p holds
( x .. p = len p iff p |-- x = {} )
let x be object ; :: thesis: ( x in rng p implies ( x .. p = len p iff p |-- x = {} ) )
assume A1: x in rng p ; :: thesis: ( x .. p = len p iff p |-- x = {} )
thus ( x .. p = len p implies p |-- x = {} ) :: thesis: ( p |-- x = {} implies x .. p = len p )

proof

assume A2: x .. p = len p ; :: thesis: p |-- x = {}
len (p |-- x) = (len p) - (x .. p) by A1, Def6
.= 0 by A2 ;
hence p |-- x = {} ; :: thesis: verum

end;

assume p |-- x = {} ; :: thesis: x .. p = len p
then A3: len (p |-- x) = 0 ;
len (p |-- x) = (len p) - (x .. p) by A1, Def6;
hence x .. p = len p by A3; :: thesis: verum