let A be preIfWhileAlgebra; for C, I1, I2 being Element of A holds if-then-else (C,I1,I2) nin ElementaryInstructions A
let C, I1, I2 be Element of A; if-then-else (C,I1,I2) nin ElementaryInstructions A
set I = if-then-else (C,I1,I2);
reconsider f = the charact of A . 3 as non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of A *), the carrier of A by Def12;
3 in dom the charact of A
by Def12;
then
In (3,(dom the charact of A)) = 3
by SUBSET_1:def 8;
then dom (Den ((In (3,(dom the charact of A))),A)) =
(arity f) -tuples_on the carrier of A
by COMPUT_1:22
.=
3 -tuples_on the carrier of A
by COMPUT_1:def 21
;
then
<*C,I1,I2*> in dom (Den ((In (3,(dom the charact of A))),A))
by FINSEQ_2:139;
then
if-then-else (C,I1,I2) in rng (Den ((In (3,(dom the charact of A))),A))
by FUNCT_1:def 3;
then
if-then-else (C,I1,I2) nin ( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))
by XBOOLE_0:def 5;
then
if-then-else (C,I1,I2) 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
if-then-else (C,I1,I2) nin ElementaryInstructions A
by XBOOLE_0:def 5; verum