theorem Th17: :: AOFA_I00:17

for f being INT-Exec
for v being INT-Variable of NAT holds v is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f