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 c = the Enumeration of X;

set f = the INT-Exec of the Enumeration of X,T;

take the INT-Exec of the Enumeration of X,T ; :: thesis: the INT-Exec of the Enumeration of X,T is Euclidean

thus the INT-Exec of the Enumeration of X,T is Euclidean ; :: thesis: verum

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 c = the Enumeration of X;

set f = the INT-Exec of the Enumeration of X,T;

take the INT-Exec of the Enumeration of X,T ; :: thesis: the INT-Exec of the Enumeration of X,T is Euclidean

thus the INT-Exec of the Enumeration of X,T is Euclidean ; :: thesis: verum