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, FUNCT_7:def 1;
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, FUNCT_7:def 1;
A8:
<*C,I1,I2*> in 3 -tuples_on the carrier of A
by FINSEQ_2:159;
A9:
<*D,J1,J2*> in 3 -tuples_on the carrier of A
by FINSEQ_2:159;
A10:
rng <*C,I1,I2*> = {C,I1,I2}
by FINSEQ_2:148;
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:157;
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:99; verum