let A be preIfWhileAlgebra; for C, I being Element of A holds while (C,I) nin ElementaryInstructions A
let C, I1 be Element of A; 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; verum