set X = NAT ;
set S = ECIW-signature ;
set G = INT-ElemIns ;
set A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ;
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
consider v being INT-Variable of NAT ;
let t be INT-Expression of NAT ; :: thesis: t is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f
AA: ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) = FreeGenSetNSG ECIW-signature ,INT-ElemIns by AOFA_000:70;
BB: Terminals (DTConUA ECIW-signature ,INT-ElemIns ) = INT-ElemIns by FREEALG:3;
reconsider v' = v as Element of Funcs (Funcs NAT ,INT ),NAT by FUNCT_2:11;
reconsider t' = t as Element of Funcs (Funcs NAT ,INT ),INT by FUNCT_2:11;
CC: [v',t'] in INT-ElemIns by ZFMISC_1:106;
then root-tree [v',t'] in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) by AA, BB;
then reconsider I = root-tree [v',t'] 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 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

proof

thus I in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) by AA, BB, CC; :: 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 v ; :: thesis: 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 t ; :: thesis: for s being Element of Funcs NAT ,INT holds f . s,I = s +* (v . s),(t . s)
thus for s being Element of Funcs NAT ,INT holds f . s,I = s +* (v . s),(t . s) by INTiwaEXEC; :: thesis: verum

end;

end;

take v ; :: thesis: v,t form_assignment_wrt f
thus v,t form_assignment_wrt f by II1; :: thesis: verum