let p be FinSequence; :: thesis: for n being natural number holds
( n in dom p iff ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) )
let n be natural number ; :: thesis: ( n in dom p iff ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) )
thus ( n in dom p implies ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) ) :: thesis: ( n - 1 is Element of NAT & (len p) - n is Element of NAT implies n in dom p )

proof

assume n in dom p ; :: thesis: ( n - 1 is Element of NAT & (len p) - n is Element of NAT )
then ( 1 <= n & n <= len p & 1 is Integer & n is Integer & len p is Integer ) by Th27;
hence ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) by INT_1:18; :: thesis: verum

end;

assume ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) ; :: thesis: n in dom p
then ( 0 + 1 <= n & 0 + n <= len p ) by XREAL_1:21;
hence n in dom p by Th27; :: thesis: verum