let P be non empty FinSequence-membered set ; :: thesis: for p being FinSequence
for n being Nat holds
( p in P |` n iff ( p in P & len p <= n ) )
let p be FinSequence; :: thesis: for n being Nat holds
( p in P |` n iff ( p in P & len p <= n ) )
let n be Nat; :: thesis: ( p in P |` n iff ( p in P & len p <= n ) )
thus ( p in P |` n implies ( p in P & len p <= n ) ) :: thesis: ( p in P & len p <= n implies p in P |` n )

proof

assume p in P |` n ; :: thesis: ( p in P & len p <= n )
then consider q being Element of P such that
A1: p = q and
A2: len q <= n ;
thus ( p in P & len p <= n ) by A1, A2; :: thesis: verum

end;

assume ( p in P & len p <= n ) ; :: thesis: p in P |` n
hence p in P |` n ; :: thesis: verum