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