let a, b be Int-Location ; :: thesis: InsCode (Divide a,b) = 5
ex A, B being Data-Location st
( a = A & b = B & Divide a,b = Divide A,B ) by Def15;
hence InsCode (Divide a,b) = 5 by MCART_1:7; :: thesis: verum