let a1, a2, b1, b2 be Int-Location; :: thesis: ( AddTo (a1,b1) = AddTo (a2,b2) implies ( a1 = a2 & b1 = b2 ) )

assume A1: AddTo (a1,b1) = AddTo (a2,b2) ; :: thesis: ( a1 = a2 & b1 = b2 )

consider A1, B1 being Data-Location such that

A2: ( a1 = A1 & b1 = B1 & AddTo (a1,b1) = AddTo (A1,B1) ) by SCMFSA_2:def 9;

consider A2, B2 being Data-Location such that

A3: ( a2 = A2 & b2 = B2 & AddTo (a2,b2) = AddTo (A2,B2) ) by SCMFSA_2:def 9;

A4: ( <*A2,B2*> . 1 = A2 & <*A2,B2*> . 2 = B2 ) by FINSEQ_1:44;

( <*A1,B1*> . 1 = A1 & <*A1,B1*> . 2 = B1 ) by FINSEQ_1:44;

hence ( a1 = a2 & b1 = b2 ) by A1, A2, A3, A4, XTUPLE_0:3; :: thesis: verum

assume A1: AddTo (a1,b1) = AddTo (a2,b2) ; :: thesis: ( a1 = a2 & b1 = b2 )

consider A1, B1 being Data-Location such that

A2: ( a1 = A1 & b1 = B1 & AddTo (a1,b1) = AddTo (A1,B1) ) by SCMFSA_2:def 9;

consider A2, B2 being Data-Location such that

A3: ( a2 = A2 & b2 = B2 & AddTo (a2,b2) = AddTo (A2,B2) ) by SCMFSA_2:def 9;

A4: ( <*A2,B2*> . 1 = A2 & <*A2,B2*> . 2 = B2 ) by FINSEQ_1:44;

( <*A1,B1*> . 1 = A1 & <*A1,B1*> . 2 = B1 ) by FINSEQ_1:44;

hence ( a1 = a2 & b1 = b2 ) by A1, A2, A3, A4, XTUPLE_0:3; :: thesis: verum