let x1, x2, x3, x4, y1, y2, y3, y4 be Real; :: thesis: [*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*]
[*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*x1,x2,x3,x4*] + [*(- y1),(- y2),(- y3),(- y4)*] by Th4
.= [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*] by QUATERNI:def 7 ;
hence [*x1,x2,x3,x4*] - [*y1,y2,y3,y4*] = [*(x1 - y1),(x2 - y2),(x3 - y3),(x4 - y4)*] ; :: thesis: verum