let m be Element of NAT ; :: thesis: for j being Integer st inspos m = j holds
inspos (m + 2) = (abs j) + 2
let j be Integer; :: thesis: ( inspos m = j implies inspos (m + 2) = (abs j) + 2 )
assume inspos m = j ; :: thesis: inspos (m + 2) = (abs j) + 2
then A1: j = il. m
.= m ;
then j >= 0 by NAT_1:2;
hence (abs j) + 2 = m + 2 by A1, ABSVALUE:def 1
.= il. (m + 2)
.= inspos (m + 2) ;
:: thesis: verum