reconsider m1 = IC s as Element of NAT ;
consider k being Element of NAT such that
A1: m1 = k ;
reconsider m = |.(k + c).| as Nat ;
reconsider l = m as Element of NAT ;
take l ; :: thesis: ex m being Element of NAT st
( m = IC s & l = |.(m + c).| )
thus ex m being Element of NAT st
( m = IC s & l = |.(m + c).| ) by A1; :: thesis: verum