theorem Th21: :: AOFA_I00:21

for X being non empty countable set
for T being Subset of (Funcs (X,INT))
for c being Enumeration of X
for f being INT-Exec of c,T
for t being INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f