theorem Th16: :: AOFA_I00:16

for f being INT-Exec
for v being INT-Variable of NAT
for t being INT-Expression of NAT holds v,t form_assignment_wrt f