let k, k' be Element of NAT ; :: thesis: ( x. k = v1 & x. k' = v1 implies k = k' )
assume ( x. k = v1 & x. k' = v1 ) ; :: thesis: k = k'
then ( 5 + k = v1 & 5 + k' = v1 ) by ZF_LANG:def 2;
hence k = k' by XCMPLX_1:2; :: thesis: verum