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 binary 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 FUNCT_7:def 1;
then dom (Den (In 4,(dom the charact of A)),A) = (arity f) -tuples_on the carrier of A by COMPUT_1:25
.= 2 -tuples_on the carrier of A by COMPUT_1:def 26 ;
then <*C,I1*> in dom (Den (In 4,(dom the charact of A)),A) by FINSEQ_2:157;
then while C,I1 in rng (Den (In 4,(dom the charact of A)),A) by FUNCT_1:def 5;
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