set X = NAT ;
set a = (INT --> 0 ) +* (id NAT );
A1: dom (id NAT ) = NAT by RELAT_1:71;
A2: INT \/ NAT = INT by NUMBERS:17, XBOOLE_1:12;
dom (INT --> 0 ) = INT by FUNCOP_1:19;
then A3: dom ((INT --> 0 ) +* (id NAT )) = INT by A1, A2, FUNCT_4:def 1;
A4: rng (id NAT ) = NAT by RELAT_1:71;
{0 } c= NAT by ZFMISC_1:37;
then A5: {0 } \/ NAT = NAT by XBOOLE_1:12;
rng (INT --> 0 ) = {0 } by FUNCOP_1:14;
then rng ((INT --> 0 ) +* (id NAT )) c= NAT by A4, A5, FUNCT_4:18;
then reconsider a = (INT --> 0 ) +* (id NAT ) as INT-Array of NAT by A3, FUNCT_2:4;
let f be INT-Exec ; :: thesis:
set S = ECIW-signature ;
set G = INT-ElemIns ;
set A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ;
set T = (Funcs NAT ,INT ) \ 0 ,0 ;
thus for v being INT-Variable of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f
for t being INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f holds v,t form_assignment_wrt f by Th16; :: according to AOFA_I00:def 22 :: thesis:
thus for i being integer number holds . i,NAT is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f by Th18; :: thesis:
thus for v being INT-Variable of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f holds . v is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f by Th18; :: thesis:
thus for x being Element of NAT holds ^ x is INT-Variable of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f by Th17; :: thesis:

hereby :: thesis:

take a = a; :: thesis:
dom (id NAT ) = NAT by RELAT_1:71;
hence a | (card NAT ) is one-to-one by CARD_1:84, FUNCT_4:24; :: thesis:
thus for t being INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f holds a * t is INT-Variable of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f by Th17; :: thesis:

end;

thus ( ( for t being INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f holds - t is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f ) & ( for t1, t2 being INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f holds
( t1 (#) t2 is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f & t1 + t2 is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f & t1 div t2 is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f & t1 mod t2 is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f & leq t1,t2 is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f & gt t1,t2 is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f ) ) ) by Th18; :: thesis: