let i1 be Element of NAT ; :: thesis: for a being Int-Location holds AddressPart (a =0_goto i1) = <*i1,a*>
let a be Int-Location ; :: thesis: AddressPart (a =0_goto i1) = <*i1,a*>
thus AddressPart (a =0_goto i1) = [7,<*i1,a*>] `2 by Th15
.= <*i1,a*> by MCART_1:def 2 ; :: thesis: verum