let a, b, c, d be real number ; :: 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 )
reconsider a = a, b = b, c = c, d = d as Real by XREAL_0:def 1;
(a - c) + ((b - d) * <i> ) = 0 by A1;
then ( a - c = 0 & b - d = 0 ) by Th12, Th28;
hence ( a = c & b = d ) ; :: thesis: verum