let A be preIfWhileAlgebra; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ) ) )
3 in dom the charact of A by Def12;
then A2: ( dom (Den (In 3,(dom the charact of A)),A) = 3 -tuples_on the carrier of A & In 3,(dom the charact of A) = 3 ) by Th47, FUNCT_7:def 1;
4 in dom the charact of A by Def13;
then A3: ( dom (Den (In 4,(dom the charact of A)),A) = 2 -tuples_on the carrier of A & In 4,(dom the charact of A) = 4 ) by Th48, FUNCT_7:def 1;
A4: ( <*C,I1,I2*> in 3 -tuples_on the carrier of A & <*D,J1,J2*> in 3 -tuples_on the carrier of A ) by CATALG_1:12;
rng <*C,I1,I2*> = {C,I1,I2} by FINSEQ_2:148;
then ( C in rng <*C,I1,I2*> & I1 in rng <*C,I1,I2*> & I2 in rng <*C,I1,I2*> ) by 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, A2, A4, Th38; :: thesis: ( 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 CATALG_1:10;
hence if-then-else C,I1,I2 <> while D,J1 by A1, A2, A3, A4, Th36; :: thesis: ( 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 ; :: thesis: ( C = D & I1 = J1 & I2 = J2 )
then <*C,I1,I2*> = <*D,J1,J2*> by A1, A2, A4, Th36;
hence ( C = D & I1 = J1 & I2 = J2 ) by GROUP_7:3; :: thesis: verum