let a1, a2 be Int-Location ; :: thesis: ( a1 :==1 = a2 :==1 implies a1 = a2 )
A1: <*a1*> . 1 = a1 by FINSEQ_1:57;
A2: <*a2*> . 1 = a2 by FINSEQ_1:57;
assume a1 :==1 = a2 :==1 ; :: thesis: a1 = a2
hence a1 = a2 by A1, A2, MCART_1:28; :: thesis: verum