let a, b, c, d be Real; :: thesis: ( a + (b * <i>) = c + (d * <i>) implies ( a = c & b = d ) )
assume A1: a + (b * <i>) = c + (d * <i>) ; :: thesis: ( a = c & b = d )
then (a - c) + ((b - d) * <i>) = 0 ;
then a - c = 0 by Th4, Th12;
hence ( a = c & b = d ) by A1; :: thesis: verum