let X be non empty countable set ; :: according to AOFA_I00:def 23 :: thesis: for T being Subset of (Funcs X,INT ) ex f being ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns , Funcs X,INT ,T st f is Euclidean
let T be Subset of (Funcs X,INT ); :: thesis: ex f being ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns , Funcs X,INT ,T st f is Euclidean
set A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ;
consider c being Enumeration of X;
consider f being INT-Exec of c,T;
take f ; :: thesis: f is Euclidean
thus f is Euclidean ; :: thesis: verum