let r be Quaternion; :: thesis: 0q * r = 0
consider x1, x2, x3, x4, y1, y2, y3, y4 being Real such that
A1: 0 = [*x1,x2,x3,x4*] and
r = [*y1,y2,y3,y4*] and
A2: 0q * r = [*((((x1 * y1) - (x2 * y2)) - (x3 * y3)) - (x4 * y4)),((((x1 * y2) + (x2 * y1)) + (x3 * y4)) - (x4 * y3)),((((x1 * y3) + (y1 * x3)) + (y2 * x4)) - (y4 * x2)),((((x1 * y4) + (x4 * y1)) + (x2 * y3)) - (x3 * y2))*] by QUATERNI:def 10;
A3: x1 = 0 by A1, Th11, QUATERNI:12;
A4: x2 = 0 by A1, Th11, QUATERNI:12;
A5: x3 = 0 by A1, Th11, QUATERNI:12;
x4 = 0 by A1, Th11, QUATERNI:12;
hence 0q * r = 0 by A2, A3, A4, A5, Th11; :: thesis: verum