consider I being Element of A such that
A1: I is_assignment_wrt A,X,f by B1;
consider v being INT-Variable of X, t being INT-Expression of X such that
A2: for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) by A1, Def14;
take v ; :: thesis: ex t being INT-Expression of X st v,t form_assignment_wrt f
take t ; :: 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 A1, A2, Def14; :: thesis: verum