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:157;
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:159;
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:157;
hence
EmptyIns A <> while C,I1
by A1, A2, A5, A6, Th36; verum