let a1, a2, b1, b2 be Int-Location; ( Divide (a1,b1) = Divide (a2,b2) implies ( a1 = a2 & b1 = b2 ) )
assume A1:
Divide (a1,b1) = Divide (a2,b2)
; ( a1 = a2 & b1 = b2 )
consider A1, B1 being Data-Location such that
A2:
( a1 = A1 & b1 = B1 & Divide (a1,b1) = Divide (A1,B1) )
by SCMFSA_2:def 12;
consider A2, B2 being Data-Location such that
A3:
( a2 = A2 & b2 = B2 & Divide (a2,b2) = Divide (A2,B2) )
by SCMFSA_2:def 12;
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; verum