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

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