let X be ComplexUnitarySpace; :: thesis: for x being Point of holds x, 0. X are_orthogonal
let x be Point of ; :: thesis: x, 0. X are_orthogonal
(0. X) .|. x = 0 by Th31;
hence x, 0. X are_orthogonal by Def14; :: thesis: verum