let a1, b1, a2, b2 be Int-Location ; :: thesis: ( Divide a1,b1 = Divide a2,b2 implies ( a1 = a2 & b1 = b2 ) )
assume A1: Divide a1,b1 = Divide a2,b2 ; :: thesis: ( 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 15;
consider A2, B2 being Data-Location such that
A3: ( a2 = A2 & b2 = B2 & Divide a2,b2 = Divide A2,B2 ) by SCMFSA_2:def 15;
( <*A1,B1*> . 1 = A1 & <*A1,B1*> . 2 = B1 & <*A2,B2*> . 1 = A2 & <*A2,B2*> . 2 = B2 ) by FINSEQ_1:61;
hence ( a1 = a2 & b1 = b2 ) by A1, A2, A3, ZFMISC_1:33; :: thesis: verum