let a be Real; :: thesis: for X being RealUnitarySpace
for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)
let X be RealUnitarySpace; :: thesis: for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)
let x, y be Point of X; :: thesis: (a * x) .|. y = x .|. (a * y)
(a * x) .|. y = a * (x .|. y) by Def2;
hence (a * x) .|. y = x .|. (a * y) by Def2; :: thesis: verum