let a, b be Int-Location ; :: thesis: InsCode (Divide a,b) = 5
consider A, B being Data-Location such that
( a = A & b = B ) and
A1: Divide a,b = Divide A,B by Def15;
thus InsCode (Divide a,b) = 5 by A1, MCART_1:7; :: thesis: verum