set S = ECIW-signature ;

set G = INT-ElemIns ;

let X be non empty countable set ; :: thesis: for T being Subset of (Funcs (X,INT))

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 (Funcs (X,INT)); :: 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

set v = the 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 c9 = c as Function of X,NAT by A2, FUNCT_2:2;

reconsider cv = c9 * the INT-Variable of X as Element of Funcs ((Funcs (X,INT)),NAT) by FUNCT_2:8;

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

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

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

set v1 = cv ** (c9,NAT);

set t1 = t9 ** (c9,NAT);

A4: [(cv ** (c9,NAT)),(t9 ** (c9,NAT))] in INT-ElemIns by ZFMISC_1:87;

then root-tree [(cv ** (c9,NAT)),(t9 ** (c9,NAT))] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A1, A3;

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

thus the INT-Variable of X,t form_assignment_wrt f by Th19; :: thesis: verum

set G = INT-ElemIns ;

let X be non empty countable set ; :: thesis: for T being Subset of (Funcs (X,INT))

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 (Funcs (X,INT)); :: 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

set v = the 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 c9 = c as Function of X,NAT by A2, FUNCT_2:2;

reconsider cv = c9 * the INT-Variable of X as Element of Funcs ((Funcs (X,INT)),NAT) by FUNCT_2:8;

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

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

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

set v1 = cv ** (c9,NAT);

set t1 = t9 ** (c9,NAT);

A4: [(cv ** (c9,NAT)),(t9 ** (c9,NAT))] in INT-ElemIns by ZFMISC_1:87;

then root-tree [(cv ** (c9,NAT)),(t9 ** (c9,NAT))] in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,INT-ElemIns)) by A1, A3;

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

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

take
the INT-Variable of X
; :: thesis: the INT-Variable of X,t form_assignment_wrt ftake 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

end;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 the INT-Variable of X ; :: thesis: ex t being INT-Expression of X st

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

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

for s being Element of Funcs (X,INT) holds f . (s,(root-tree [((c * v9) ** (c,NAT)),(t9 ** (c,NAT))])) = s +* ((v9 . s),(t9 . s)) by A2, Def28;

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

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

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

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

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

for s being Element of Funcs (X,INT) holds f . (s,(root-tree [((c * v9) ** (c,NAT)),(t9 ** (c,NAT))])) = s +* ((v9 . s),(t9 . s)) by A2, Def28;

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

thus the INT-Variable of X,t form_assignment_wrt f by Th19; :: thesis: verum