let l1, l2 be Element of NAT ; :: thesis: ( goto l1 = goto l2 implies l1 = l2 )
assume A1: goto l1 = goto l2 ; :: thesis: l1 = l2
( <*l1*> . 1 = l1 & <*l2*> . 1 = l2 ) by FINSEQ_1:40;
hence l1 = l2 by A1, MCART_1:25; :: thesis: verum