set S = ECIW-signature ;
set G = INT-ElemIns ;
let X be non empty countable set ; :: thesis: for T being Subset of
for c being Enumeration of X
for f being INT-Exec of c,T
for t being INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f
let T be Subset of ; :: thesis: for c being Enumeration of X
for f being INT-Exec of c,T
for t being INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f
let c be Enumeration of X; :: thesis: for f being INT-Exec of c,T
for t being INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f
set A = FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ;
let f be INT-Exec of c,T; :: thesis: for t being INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f
consider v being INT-Variable of X;
let t be INT-Expression of X; :: thesis: t is INT-Expression of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,f
A1: ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) = FreeGenSetNSG ECIW-signature ,INT-ElemIns by AOFA_000:70;
A2: rng c c= NAT by Th11;
dom c = X by Th6;
then reconsider c' = c as Function of X, NAT by A2, FUNCT_2:4;
reconsider cv = c' * v as Element of Funcs (Funcs X,INT ),NAT by FUNCT_2:11;
reconsider v' = v as Element of Funcs (Funcs X,INT ),X by FUNCT_2:11;
reconsider t' = t as Element of Funcs (Funcs X,INT ),INT by FUNCT_2:11;
A3: Terminals (DTConUA ECIW-signature ,INT-ElemIns ) = INT-ElemIns by FREEALG:3;
set v1 = cv ** c',NAT ;
set t1 = t' ** c',NAT ;
A4: [(cv ** c',NAT ),(t' ** c',NAT )] in INT-ElemIns by ZFMISC_1:106;
then root-tree [(cv ** c',NAT ),(t' ** c',NAT )] in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) by A1, A3;
then reconsider I = root-tree [(cv ** c',NAT ),(t' ** c',NAT )] as Element of ;

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

take I = I; :: thesis: I is_assignment_wrt FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,X,f
thus I is_assignment_wrt FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ,X,f :: thesis: verum

proof

thus I in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,INT-ElemIns ) by A1, A3, A4; :: according to AOFA_I00:def 14 :: thesis: ex v being INT-Variable of X ex t being INT-Expression of X st
for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s)
take v ; :: thesis: ex t being INT-Expression of X st
for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s)
take t ; :: thesis: for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s)
for s being Element of Funcs X,INT holds f . s,(root-tree [((c * v') ** c,NAT ),(t' ** c,NAT )]) = s +* (v' . s),(t' . s) by A2, Def28;
hence for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ; :: thesis: verum

end;

end;

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