theorem Th18: :: AOFA_I00:18

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