consider I being Element of A such that
A2: I is_assignment_wrt A,X,f by A1;
consider v being INT-Variable of X, t being INT-Expression of X such that
A3: for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) by A2, Def14;
take t ; :: thesis: ex v being INT-Variable of X st v,t form_assignment_wrt f
take v ; :: thesis: v,t form_assignment_wrt f
take I ; :: according to AOFA_I00:def 15 :: thesis: ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) )
thus ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) by A2, A3, Def14; :: thesis: verum