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, SUBSET_1:def 8;
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, SUBSET_1:def 8;
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, SUBSET_1:def 8;
A11:
<*I1,I2*> in 2 -tuples_on the carrier of A
by FINSEQ_2:137;
A12:
<*J1,J2*> in 2 -tuples_on the carrier of A
by FINSEQ_2:137;
A13:
rng <*I1,I2*> = {I1,I2}
by FINSEQ_2:127;
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:139;
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:137;
hence
I1 \; I2 <> while (C,J1)
by A1, A3, A4, A9, A10, A11, Th36; verum