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