A1: rng c c= NAT by Th11;
card X = rng c by Th6;
then A2: INT \/ (card X) = INT by A1, NUMBERS:17, XBOOLE_1:1, XBOOLE_1:12;
set x = (c " ) . 0 ;
set a = (INT --> ((c " ) . 0 )) +* (c " );
A3: dom (INT --> ((c " ) . 0 )) = INT by FUNCOP_1:19;
A4: rng (INT --> ((c " ) . 0 )) = {((c " ) . 0 )} by FUNCOP_1:14;
(c " ) . 0 in X by FUNCT_2:7, ORDINAL3:10;
then {((c " ) . 0 )} c= X by ZFMISC_1:37;
then A5: {((c " ) . 0 )} \/ X = X by XBOOLE_1:12;
rng (c " ) = X by Th7;
then A6: rng ((INT --> ((c " ) . 0 )) +* (c " )) c= X by A4, A5, FUNCT_4:18;
dom (c " ) = card X by Th7;
then dom ((INT --> ((c " ) . 0 )) +* (c " )) = INT by A3, A2, FUNCT_4:def 1;
then reconsider a = (INT --> ((c " ) . 0 )) +* (c " ) as INT-Array of X by A6, FUNCT_2:4;
let f be INT-Exec of c,T; :: thesis:
set S = ECIW-signature ;
set G = INT-ElemIns ;
set A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ;
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 Th19; :: according to AOFA_I00:def 22 :: thesis:
thus for i being integer number holds . i,X is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f by Th21; :: 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 Th21; :: thesis:
thus for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f by Th20; :: thesis:

hereby :: thesis:

take a = a; :: thesis:
dom (c " ) = card X by Th7;
hence a | (card X) is one-to-one by 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 Th20; :: 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 Th21; :: thesis: