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