let k, n be odd Element of NAT ; :: thesis: n + (k -' 1) is odd Element of NAT
consider i being Nat such that
A1: k = (2 * i) + 1 by ABIAN:9;
consider j being Nat such that
A2: n = (2 * j) + 1 by ABIAN:9;
n + (k -' 1) = ((2 * j) + 1) + (2 * i) by A1, A2, NAT_D:34
.= (2 * (j + i)) + 1 ;
hence n + (k -' 1) is odd Element of NAT ; :: thesis: verum