let A be preIfWhileAlgebra; ( A is free implies for I1, I2, C, J1, J2 being Element of A holds
( I1 \; I2 <> I1 & I1 \; I2 <> I2 & ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 & I2 = J2 ) ) & I1 \; I2 <> if-then-else C,J1,J2 & I1 \; I2 <> while C,J1 ) )
assume A1:
A is free
; for I1, I2, C, J1, J2 being Element of A holds
( I1 \; I2 <> I1 & I1 \; I2 <> I2 & ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 & I2 = J2 ) ) & I1 \; I2 <> if-then-else C,J1,J2 & I1 \; I2 <> while C,J1 )
let I1, I2, C, J1, J2 be Element of A; ( I1 \; I2 <> I1 & I1 \; I2 <> I2 & ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 & I2 = J2 ) ) & I1 \; I2 <> if-then-else C,J1,J2 & I1 \; I2 <> while C,J1 )
A2:
2 in dom the charact of A
by Def11;
A3:
dom (Den (In 2,(dom the charact of A)),A) = 2 -tuples_on the carrier of A
by Th44;
A4:
In 2,(dom the charact of A) = 2
by A2, FUNCT_7:def 1;
A5:
3 in dom the charact of A
by Def12;
A6:
dom (Den (In 3,(dom the charact of A)),A) = 3 -tuples_on the carrier of A
by Th47;
A7:
In 3,(dom the charact of A) = 3
by A5, FUNCT_7:def 1;
A8:
4 in dom the charact of A
by Def13;
A9:
dom (Den (In 4,(dom the charact of A)),A) = 2 -tuples_on the carrier of A
by Th48;
A10:
In 4,(dom the charact of A) = 4
by A8, FUNCT_7:def 1;
A11:
<*I1,I2*> in 2 -tuples_on the carrier of A
by FINSEQ_2:157;
A12:
<*J1,J2*> in 2 -tuples_on the carrier of A
by FINSEQ_2:157;
A13:
rng <*I1,I2*> = {I1,I2}
by FINSEQ_2:147;
then A14:
I1 in rng <*I1,I2*>
by TARSKI:def 2;
I2 in rng <*I1,I2*>
by A13, TARSKI:def 2;
hence
( I1 \; I2 <> I1 & I1 \; I2 <> I2 )
by A1, A3, A11, A14, Th38; ( ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 & I2 = J2 ) ) & I1 \; I2 <> if-then-else C,J1,J2 & I1 \; I2 <> while C,J1 )
<*C,J1,J2*> in 3 -tuples_on the carrier of A
by FINSEQ_2:159;
hence
I1 \; I2 <> if-then-else C,J1,J2
by A1, A3, A4, A6, A7, A11, Th36; I1 \; I2 <> while C,J1
<*C,J1*> in 2 -tuples_on the carrier of A
by FINSEQ_2:157;
hence
I1 \; I2 <> while C,J1
by A1, A3, A4, A9, A10, A11, Th36; verum