let a, b be Int-Location ; :: thesis: Divide a,b = [5,{} ,<*a,b*>]
ex A, B being Data-Location st
( a = A & b = B & Divide a,b = Divide A,B ) by SCMFSA_2:def 15;
hence Divide a,b = [5,{} ,<*a,b*>] ; :: thesis: verum