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