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) ) ) } ;
v,t form_assignment_wrt f by INT'iwa;
then consider I0 being Element of A such that
A0: I0 in ElementaryInstructions A and
A1: for s being Element of Funcs X,INT holds f . s,I0 = s +* (v . s),(t . s) by FA;
A2: { 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;

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 A0, A1;
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 A2; :: thesis: verum