let V be RealNormSpace; :: thesis: for x being Point of V
for y being Point of (DualSp V)
for a being Real holds (a * x) .|. y = a * (x .|. y)
let x be Point of V; :: thesis: for y being Point of (DualSp V)
for a being Real holds (a * x) .|. y = a * (x .|. y)
let y be Point of (DualSp V); :: thesis: for a being Real holds (a * x) .|. y = a * (x .|. y)
let a be Real; :: thesis: (a * x) .|. y = a * (x .|. y)
reconsider y1 = y as linear-Functional of V by DUALSP01:def 10;
thus (a * x) .|. y = y1 . (a * x)
.= a * (x .|. y) by HAHNBAN:def 3 ; :: thesis: verum