let n be set ; :: thesis: for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )
let p be FinSequence; :: thesis: ( n in dom p implies ex k being Element of NAT st
( n = k + 1 & k < len p ) )
assume A1: n in dom p ; :: thesis: ex k being Element of NAT st
( n = k + 1 & k < len p )
then reconsider n = n as Element of NAT ;
n >= 1 by A1, FINSEQ_3:25;
then consider k being Nat such that
A2: n = 1 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: ( n = k + 1 & k < len p )
n <= len p by A1, FINSEQ_3:25;
hence ( n = k + 1 & k < len p ) by A2, NAT_1:13; :: thesis: verum