let A be preIfWhileAlgebra; :: thesis: 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; :: thesis: 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 ternary 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 FUNCT_7:def 1;
then dom (Den (In 3,(dom the charact of A)),A) = (arity f) -tuples_on the carrier of A by COMPUT_1:25
.= 3 -tuples_on the carrier of A by COMPUT_1:def 27 ;
then <*C,I1,I2*> in dom (Den (In 3,(dom the charact of A)),A) by FINSEQ_2:159;
then if-then-else C,I1,I2 in rng (Den (In 3,(dom the charact of A)),A) by FUNCT_1: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)) 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; :: thesis: verum