let c1, c2, c3 be Complex; :: thesis: <*c1,c2,c3*> " = <*(c1 "),(c2 "),(c3 ")*>
A1: <*c1,c2*> " = <*(c1 "),(c2 ")*> by Th64;
<*c3*> " = <*(c3 ")*> by Th63;
hence <*c1,c2,c3*> " = <*(c1 "),(c2 "),(c3 ")*> by A1, Th60; :: thesis: verum