let m, n be Element of NAT ; :: thesis: ( prop n = prop m implies n = m )
assume prop n = prop m ; :: thesis: n = m
then 3 + n = 3 + m by FINSEQ_1:76;
hence n = m ; :: thesis: verum