let A be preIfWhileAlgebra; ( A is free implies for C, I1, I2, D, J1, J2 being Element of A holds
( if-then-else (C,I1,I2) <> C & if-then-else (C,I1,I2) <> I1 & if-then-else (C,I1,I2) <> I2 & if-then-else (C,I1,I2) <> while (D,J1) & ( if-then-else (C,I1,I2) = if-then-else (D,J1,J2) implies ( C = D & I1 = J1 & I2 = J2 ) ) ) )
assume A1:
A is free
; for C, I1, I2, D, J1, J2 being Element of A holds
( if-then-else (C,I1,I2) <> C & if-then-else (C,I1,I2) <> I1 & if-then-else (C,I1,I2) <> I2 & if-then-else (C,I1,I2) <> while (D,J1) & ( if-then-else (C,I1,I2) = if-then-else (D,J1,J2) implies ( C = D & I1 = J1 & I2 = J2 ) ) )
let C, I1, I2, D, J1, J2 be Element of A; ( if-then-else (C,I1,I2) <> C & if-then-else (C,I1,I2) <> I1 & if-then-else (C,I1,I2) <> I2 & if-then-else (C,I1,I2) <> while (D,J1) & ( if-then-else (C,I1,I2) = if-then-else (D,J1,J2) implies ( C = D & I1 = J1 & I2 = J2 ) ) )
A2:
3 in dom the charact of A
by Def12;
A3:
dom (Den ((In (3,(dom the charact of A))),A)) = 3 -tuples_on the carrier of A
by Th47;
A4:
In (3,(dom the charact of A)) = 3
by A2, SUBSET_1:def 8;
A5:
4 in dom the charact of A
by Def13;
A6:
dom (Den ((In (4,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A
by Th48;
A7:
In (4,(dom the charact of A)) = 4
by A5, SUBSET_1:def 8;
A8:
<*C,I1,I2*> in 3 -tuples_on the carrier of A
by FINSEQ_2:139;
A9:
<*D,J1,J2*> in 3 -tuples_on the carrier of A
by FINSEQ_2:139;
A10:
rng <*C,I1,I2*> = {C,I1,I2}
by FINSEQ_2:128;
then A11:
C in rng <*C,I1,I2*>
by ENUMSET1:def 1;
A12:
I1 in rng <*C,I1,I2*>
by A10, ENUMSET1:def 1;
I2 in rng <*C,I1,I2*>
by A10, ENUMSET1:def 1;
hence
( if-then-else (C,I1,I2) <> C & if-then-else (C,I1,I2) <> I1 & if-then-else (C,I1,I2) <> I2 )
by A1, A3, A8, A11, A12, Th38; ( if-then-else (C,I1,I2) <> while (D,J1) & ( if-then-else (C,I1,I2) = if-then-else (D,J1,J2) implies ( C = D & I1 = J1 & I2 = J2 ) ) )
<*D,J1*> in 2 -tuples_on the carrier of A
by FINSEQ_2:137;
hence
if-then-else (C,I1,I2) <> while (D,J1)
by A1, A3, A4, A6, A7, A8, Th36; ( if-then-else (C,I1,I2) = if-then-else (D,J1,J2) implies ( C = D & I1 = J1 & I2 = J2 ) )
assume
if-then-else (C,I1,I2) = if-then-else (D,J1,J2)
; ( C = D & I1 = J1 & I2 = J2 )
then
<*C,I1,I2*> = <*D,J1,J2*>
by A1, A3, A8, A9, Th36;
hence
( C = D & I1 = J1 & I2 = J2 )
by FINSEQ_1:78; verum