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 ) 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