let A be preIfWhileAlgebra; ( A is free implies for C, I1, I2 being Element of A holds
( EmptyIns A <> I1 \; I2 & EmptyIns A <> if-then-else (C,I1,I2) & EmptyIns A <> while (C,I1) ) )
assume A1:
A is free
; for C, I1, I2 being Element of A holds
( EmptyIns A <> I1 \; I2 & EmptyIns A <> if-then-else (C,I1,I2) & EmptyIns A <> while (C,I1) )
let C, I1, I2 be Element of A; ( EmptyIns A <> I1 \; I2 & EmptyIns A <> if-then-else (C,I1,I2) & EmptyIns A <> while (C,I1) )
A2:
dom (Den ((In (1,(dom the charact of A))),A)) = {{}}
by Th42;
A3:
dom (Den ((In (2,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A
by Th44;
A4:
dom (Den ((In (3,(dom the charact of A))),A)) = 3 -tuples_on the carrier of A
by Th47;
A5:
dom (Den ((In (4,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A
by Th48;
A6:
{} in {{}}
by TARSKI:def 1;
<*I1,I2*> in 2 -tuples_on the carrier of A
by FINSEQ_2:137;
hence
EmptyIns A <> I1 \; I2
by A1, A2, A3, A6, Th36; ( EmptyIns A <> if-then-else (C,I1,I2) & EmptyIns A <> while (C,I1) )
<*C,I1,I2*> in 3 -tuples_on the carrier of A
by FINSEQ_2:139;
hence
EmptyIns A <> if-then-else (C,I1,I2)
by A1, A2, A4, A6, Th36; EmptyIns A <> while (C,I1)
<*C,I1*> in 2 -tuples_on the carrier of A
by FINSEQ_2:137;
hence
EmptyIns A <> while (C,I1)
by A1, A2, A5, A6, Th36; verum