let A be preIfWhileAlgebra; :: thesis: ( A is free implies for C, I, D, J being Element of A holds
( while (C,I) <> C & while (C,I) <> I & ( while (C,I) = while (D,J) implies ( C = D & I = J ) ) ) )
assume A1: A is free ; :: thesis: for C, I, D, J being Element of A holds
( while (C,I) <> C & while (C,I) <> I & ( while (C,I) = while (D,J) implies ( C = D & I = J ) ) )
let C, I, D, J be Element of A; :: thesis: ( while (C,I) <> C & while (C,I) <> I & ( while (C,I) = while (D,J) implies ( C = D & I = J ) ) )
A2: dom (Den ((In (4,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A by Th48;
A3: <*C,I*> in 2 -tuples_on the carrier of A by FINSEQ_2:137;
A4: <*D,J*> in 2 -tuples_on the carrier of A by FINSEQ_2:137;
A5: rng <*C,I*> = {C,I} by FINSEQ_2:127;
then A6: C in rng <*C,I*> by TARSKI:def 2;
I in rng <*C,I*> by A5, TARSKI:def 2;
hence ( while (C,I) <> C & while (C,I) <> I ) by A1, A2, A3, A6, Th38; :: thesis: ( while (C,I) = while (D,J) implies ( C = D & I = J ) )
assume while (C,I) = while (D,J) ; :: thesis: ( C = D & I = J )
then <*C,I*> = <*D,J*> by A1, A2, A3, A4, Th36;
hence ( C = D & I = J ) by FINSEQ_1:77; :: thesis: verum