set Y = { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } ;
A1: { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } c= the carrier of A

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } or i in the carrier of A )
assume i in { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } ; :: thesis: i in the carrier of A
then ex I being Element of A st
( i = I & I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) ;
hence i in the carrier of A ; :: thesis: verum

end;

v,t form_assignment_wrt f by Def22;
then consider I0 being Element of A such that
A2: I0 in ElementaryInstructions A and
A3: for s being Element of Funcs X,INT holds f . s,I0 = s +* (v . s),(t . s) by Def15;
I0 in { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } by A2, A3;
then choose { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } in { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } ;
hence choose { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } is Element of A by A1; :: thesis: verum