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 Def10;
hence InsCode (Divide (a,b)) = 5 ; :: thesis: verum