dom c = X by Th6;
then reconsider c9 = c as Function of X,NAT by A1, FUNCT_2:2;
reconsider i0 = 0 as Element of INT by INT_1:def 1;
set Q = Funcs (X,INT);
set S = ECIW-signature ;
set G = INT-ElemIns ;
set A = FreeUnivAlgNSG (ECIW-signature,INT-ElemIns);
reconsider q0 = X --> i0 as Element of Funcs (X,INT) by FUNCT_2:8;
A2: Terminals (DTConUA (ECIW-signature,INT-ElemIns)) = INT-ElemIns by FREEALG:3;
defpred S₁[ object , object ] means ex s being Element of Funcs (X,INT) st
( $1 `1 = s & ( ( $2 = s & ( for v being Element of Funcs ((Funcs (X,INT)),X)
for e being Element of Funcs ((Funcs (X,INT)),INT) holds not $1 `2 = root-tree [((c * v) ** (c9,NAT)),(e ** (c9,NAT))] ) ) or ex v being Element of Funcs ((Funcs (X,INT)),X) ex e being Element of Funcs ((Funcs (X,INT)),INT) st
( $1 `2 = root-tree [((c * v) ** (c9,NAT)),(e ** (c9,NAT))] & $2 = s +* ((v . s),(e . s)) ) ) );
A3: ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) = FreeGenSetNSG (ECIW-signature,INT-ElemIns) by AOFA_000:70;
A4: for x being object st x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] holds
ex y being object st
( y in Funcs (X,INT) & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] ; :: thesis:
then consider s, I being object such that
A5: s in Funcs (X,INT) and
A6: I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) and
A7: x = [s,I] by ZFMISC_1:def 2;
A8: x `1 = s by A7;
reconsider s = s as Element of Funcs (X,INT) by A5;
A9: x `2 = I by A7;
consider a being Symbol of (DTConUA (ECIW-signature,INT-ElemIns)) such that
A10: I = root-tree a and
a in Terminals (DTConUA (ECIW-signature,INT-ElemIns)) by A3, A6;

per cases ;

suppose ex v being Element of Funcs ((Funcs (X,INT)),X) ex e being Element of Funcs ((Funcs (X,INT)),INT) st a = [((c * v) ** (c9,NAT)),(e ** (c9,NAT))] ; :: thesis:

then consider v being Element of Funcs ((Funcs (X,INT)),X), e being Element of Funcs ((Funcs (X,INT)),INT) such that
A11: a = [((c * v) ** (c9,NAT)),(e ** (c9,NAT))] ;
take y = s +* ((v . s),(e . s)); :: thesis:
thus y in Funcs (X,INT) by FUNCT_2:8; :: thesis:
thus S₁[x,y] by A8, A9, A10, A11; :: thesis:

end;

suppose A12: for v being Element of Funcs ((Funcs (X,INT)),X)
for e being Element of Funcs ((Funcs (X,INT)),INT) holds not a = [((c * v) ** (c9,NAT)),(e ** (c9,NAT))] ; :: thesis:

take y = s; :: thesis:
thus y in Funcs (X,INT) ; :: thesis:
for v being Element of Funcs ((Funcs (X,INT)),X)
for e being Element of Funcs ((Funcs (X,INT)),INT) holds not x `2 = root-tree [((c * v) ** (c9,NAT)),(e ** (c9,NAT))] by A9, A10, A12, TREES_4:4;
hence S₁[x,y] by A8; :: thesis:

end;

consider g being Function such that
A13: ( dom g = [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] & rng g c= Funcs (X,INT) ) and
A14: for x being object st x in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] holds
S₁[x,g . x] from FUNCT_1:sch 6(A4);
reconsider g = g as Function of [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):],(Funcs (X,INT)) by A13, FUNCT_2:2;
consider f being ExecutionFunction of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), Funcs (X,INT),T such that
A15: f | [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] = g and
for s being Element of Funcs (X,INT)
for C, I being Element of (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = q0 by AOFA_000:91;
take f ; :: thesis:
let s be Element of Funcs (X,INT); :: thesis:
let v be Element of Funcs ((Funcs (X,INT)),X); :: thesis:
let e be Element of Funcs ((Funcs (X,INT)),INT); :: thesis:
reconsider vv = v as Function of (Funcs (X,INT)),X ;
reconsider cv = c9 * vv as Element of Funcs ((Funcs (X,INT)),NAT) by FUNCT_2:8;
set v0 = cv ** (c9,NAT);
set e0 = e ** (c9,NAT);
set I = root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))];
[(cv ** (c9,NAT)),(e ** (c9,NAT))] in INT-ElemIns by ZFMISC_1:87;
then root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A3, A2;
then A16: [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] in [:(Funcs (X,INT)),(ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))):] by ZFMISC_1:87;
then S₁[[s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])],g . [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])]] by A14;
then consider v9 being Element of Funcs ((Funcs (X,INT)),X), e9 being Element of Funcs ((Funcs (X,INT)),INT) such that
A17: [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] `2 = root-tree [((c * v9) ** (c9,NAT)),(e9 ** (c9,NAT))] and
A18: g . [s,(root-tree [(cv ** (c9,NAT)),(e ** (c9,NAT))])] = s +* ((v9 . s),(e9 . s)) ;
A19: dom (c9 * v9) = Funcs (X,INT) by FUNCT_2:def 1;
A20: dom e = Funcs (X,INT) by FUNCT_2:def 1;
A21: dom v = Funcs (X,INT) by FUNCT_2:def 1;
A22: dom cv = Funcs (X,INT) by FUNCT_2:def 1;
A23: dom c9 = X by FUNCT_2:def 1;
A24: rng v c= X ;
A25: dom e9 = Funcs (X,INT) by FUNCT_2:def 1;
A26: dom v9 = Funcs (X,INT) by FUNCT_2:def 1;
A27: [(cv ** (c9,NAT)),(e ** (c9,NAT))] = [((c * v9) ** (c9,NAT)),(e9 ** (c9,NAT))] by A17, TREES_4:4;
then cv ** (c9,NAT) = (c * v9) ** (c9,NAT) by XTUPLE_0:1;
then A28: cv = c * v9 by A22, A19, Th5;
e ** (c9,NAT) = e9 ** (c9,NAT) by A27, XTUPLE_0:1;
then A29: e = e9 by A20, A25, Th5;
rng v9 c= X ;
then v = v9 by A24, A23, A26, A21, A28, FUNCT_1:27;
hence f . (s,(root-tree [((c * v) ** (c,NAT)),(e ** (c,NAT))])) = s +* ((v . s),(e . s)) by A15, A16, A18, A29, FUNCT_1:49; :: thesis: