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 ;

A4: rng (INT --> ((c ") . 0)) = {((c ") . 0)} by FUNCOP_1:8;

(c ") . 0 in X by FUNCT_2:5, ORDINAL3:8;

then {((c ") . 0)} c= X by ZFMISC_1:31;

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:17;

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:2;

let f be INT-Exec of c,T; :: thesis: f is Euclidean

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: ( ( for i being Integer holds . (i,X) is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ( for v being INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f holds . v is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ( for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( 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 ) ) & ( 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 ) ) )

thus for i being Integer holds . (i,X) is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f by Th21; :: thesis: ( ( for v being INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f holds . v is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ( for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( 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 ) ) & ( 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 ) ) )

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: ( ( for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( 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 ) ) & ( 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 ) ) )

thus for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f by Th20; :: thesis: ( ex a being INT-Array of X st

( a | (card X) is one-to-one & ( 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 ) ) & ( 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 ) ) )

( 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: verum

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 ;

A4: rng (INT --> ((c ") . 0)) = {((c ") . 0)} by FUNCOP_1:8;

(c ") . 0 in X by FUNCT_2:5, ORDINAL3:8;

then {((c ") . 0)} c= X by ZFMISC_1:31;

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:17;

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:2;

let f be INT-Exec of c,T; :: thesis: f is Euclidean

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: ( ( for i being Integer holds . (i,X) is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ( for v being INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f holds . v is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ( for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( 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 ) ) & ( 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 ) ) )

thus for i being Integer holds . (i,X) is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f by Th21; :: thesis: ( ( for v being INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f holds . v is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ( for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( 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 ) ) & ( 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 ) ) )

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: ( ( for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f ) & ex a being INT-Array of X st

( a | (card X) is one-to-one & ( 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 ) ) & ( 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 ) ) )

thus for x being Element of X holds ^ x is INT-Variable of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f by Th20; :: thesis: ( ex a being INT-Array of X st

( a | (card X) is one-to-one & ( 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 ) ) & ( 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 ) ) )

hereby :: thesis: ( ( 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 ) ) )

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 ) ) )

take a = a; :: thesis: ( a | (card X) is one-to-one & ( 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 ) )

dom (c ") = card X by Th7;

hence a | (card X) is one-to-one by FUNCT_4:23; :: thesis: 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

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: verum

end;dom (c ") = card X by Th7;

hence a | (card X) is one-to-one by FUNCT_4:23; :: thesis: 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

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: verum

( 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: verum