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