let p be FinSequence; :: thesis: for n being Nat holds
( n in dom p iff ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) )
let n be Nat; :: 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 A1: n in dom p ; :: thesis: ( n - 1 is Element of NAT & (len p) - n is Element of NAT )
then A2: n <= len p by Th25;
1 <= n by A1, Th25;
hence ( n - 1 is Element of NAT & (len p) - n is Element of NAT ) by A2, INT_1:5; :: thesis: verum

end;

assume that
A3: n - 1 is Element of NAT and
A4: (len p) - n is Element of NAT ; :: thesis: n in dom p
A5: 0 + n <= len p by A4, XREAL_1:19;
0 + 1 <= n by A3, XREAL_1:19;
hence n in dom p by A5, Th25; :: thesis: verum