let A be preIfWhileAlgebra; :: thesis: for C, I being Element of A holds while (C,I) nin ElementaryInstructions A
let C, I1 be Element of A; :: thesis: while (C,I1) nin ElementaryInstructions A
set I = while (C,I1);
reconsider f = the charact of A . 4 as non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A by Def13;
4 in dom the charact of A by Def13;
then In (4,(dom the charact of A)) = 4 by SUBSET_1:def 8;
then dom (Den ((In (4,(dom the charact of A))),A)) = (arity f) -tuples_on the carrier of A by COMPUT_1:22
.= 2 -tuples_on the carrier of A by COMPUT_1:def 21 ;
then <*C,I1*> in dom (Den ((In (4,(dom the charact of A))),A)) by FINSEQ_2:137;
then while (C,I1) in rng (Den ((In (4,(dom the charact of A))),A)) by FUNCT_1:def 3;
then while (C,I1) nin (( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))) \ (rng (Den ((In (4,(dom the charact of A))),A))) by XBOOLE_0:def 5;
hence while (C,I1) nin ElementaryInstructions A by XBOOLE_0:def 5; :: thesis: verum