let A be preIfWhileAlgebra; :: thesis:
assume A1: A is free ; :: thesis:
let C, I1, I2 be Element of A; :: thesis:
1 in dom the charact of A by Def10;
then A2: ( dom (Den (In 1,(dom the charact of A)),A) = {{} } & In 1,(dom the charact of A) = 1 ) by Th42, FUNCT_7:def 1;
2 in dom the charact of A by Def11;
then A3: ( dom (Den (In 2,(dom the charact of A)),A) = 2 -tuples_on the carrier of A & In 2,(dom the charact of A) = 2 ) by Th44, FUNCT_7:def 1;
3 in dom the charact of A by Def12;
then A4: ( dom (Den (In 3,(dom the charact of A)),A) = 3 -tuples_on the carrier of A & In 3,(dom the charact of A) = 3 ) by Th47, FUNCT_7:def 1;
4 in dom the charact of A by Def13;
then A5: ( dom (Den (In 4,(dom the charact of A)),A) = 2 -tuples_on the carrier of A & In 4,(dom the charact of A) = 4 ) by Th48, FUNCT_7:def 1;
A6: {} in {{} } by TARSKI:def 1;
<*I1,I2*> in 2 -tuples_on the carrier of A by CATALG_1:10;
hence EmptyIns A <> I1 \; I2 by A1, A2, A3, A6, Th36; :: thesis:
<*C,I1,I2*> in 3 -tuples_on the carrier of A by CATALG_1:12;
hence EmptyIns A <> if-then-else C,I1,I2 by A1, A2, A4, A6, Th36; :: thesis:
<*C,I1*> in 2 -tuples_on the carrier of A by CATALG_1:10;
hence EmptyIns A <> while C,I1 by A1, A2, A5, A6, Th36; :: thesis: