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