set v = the INT-Variable of NAT;

let f be INT-Exec ; :: thesis: for t being INT-Expression of NAT holds t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

set S = ECIW-signature ;

set G = INT-ElemIns ;

set X = NAT ;

set A = FreeUnivAlgNSG (ECIW-signature,INT-ElemIns);

let t be INT-Expression of NAT; :: thesis: t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

A1: Terminals (DTConUA (ECIW-signature,INT-ElemIns)) = INT-ElemIns by FREEALG:3;

reconsider t9 = t as Element of Funcs ((Funcs (NAT,INT)),INT) by FUNCT_2:8;

reconsider v9 = the INT-Variable of NAT as Element of Funcs ((Funcs (NAT,INT)),NAT) by FUNCT_2:8;

A2: [v9,t9] in INT-ElemIns by ZFMISC_1:87;

A3: ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) = FreeGenSetNSG (ECIW-signature,INT-ElemIns) by AOFA_000:70;

then root-tree [v9,t9] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A1, A2;

then reconsider I = root-tree [v9,t9] as Element of (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) ;

thus the INT-Variable of NAT,t form_assignment_wrt f by Th16; :: thesis: verum

let f be INT-Exec ; :: thesis: for t being INT-Expression of NAT holds t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

set S = ECIW-signature ;

set G = INT-ElemIns ;

set X = NAT ;

set A = FreeUnivAlgNSG (ECIW-signature,INT-ElemIns);

let t be INT-Expression of NAT; :: thesis: t is INT-Expression of FreeUnivAlgNSG (ECIW-signature,INT-ElemIns),f

A1: Terminals (DTConUA (ECIW-signature,INT-ElemIns)) = INT-ElemIns by FREEALG:3;

reconsider t9 = t as Element of Funcs ((Funcs (NAT,INT)),INT) by FUNCT_2:8;

reconsider v9 = the INT-Variable of NAT as Element of Funcs ((Funcs (NAT,INT)),NAT) by FUNCT_2:8;

A2: [v9,t9] in INT-ElemIns by ZFMISC_1:87;

A3: ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) = FreeGenSetNSG (ECIW-signature,INT-ElemIns) by AOFA_000:70;

then root-tree [v9,t9] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A1, A2;

then reconsider I = root-tree [v9,t9] as Element of (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) ;

hereby :: according to AOFA_I00:def 17 :: thesis: ex v being INT-Variable of NAT st v,t form_assignment_wrt f

take
the INT-Variable of NAT
; :: thesis: the INT-Variable of NAT,t form_assignment_wrt ftake I = I; :: thesis: I is_assignment_wrt FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), NAT ,f

thus I is_assignment_wrt FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), NAT ,f :: thesis: verum

end;thus I is_assignment_wrt FreeUnivAlgNSG (ECIW-signature,INT-ElemIns), NAT ,f :: thesis: verum

proof

thus
I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns))
by A3, A1, A2; :: according to AOFA_I00:def 14 :: thesis: ex v being INT-Variable of NAT ex t being INT-Expression of NAT st

for s being Element of Funcs (NAT,INT) holds f . (s,I) = s +* ((v . s),(t . s))

take the INT-Variable of NAT ; :: thesis: ex t being INT-Expression of NAT st

for s being Element of Funcs (NAT,INT) holds f . (s,I) = s +* (( the INT-Variable of NAT . s),(t . s))

take t ; :: thesis: for s being Element of Funcs (NAT,INT) holds f . (s,I) = s +* (( the INT-Variable of NAT . s),(t . s))

thus for s being Element of Funcs (NAT,INT) holds f . (s,I) = s +* (( the INT-Variable of NAT . s),(t . s)) by Def25; :: thesis: verum

end;for s being Element of Funcs (NAT,INT) holds f . (s,I) = s +* ((v . s),(t . s))

take the INT-Variable of NAT ; :: thesis: ex t being INT-Expression of NAT st

for s being Element of Funcs (NAT,INT) holds f . (s,I) = s +* (( the INT-Variable of NAT . s),(t . s))

take t ; :: thesis: for s being Element of Funcs (NAT,INT) holds f . (s,I) = s +* (( the INT-Variable of NAT . s),(t . s))

thus for s being Element of Funcs (NAT,INT) holds f . (s,I) = s +* (( the INT-Variable of NAT . s),(t . s)) by Def25; :: thesis: verum

thus the INT-Variable of NAT,t form_assignment_wrt f by Th16; :: thesis: verum