let V be RealNormSpace; :: thesis: for x being Point of V
for y, z being Point of (DualSp V)
for a, b being Real holds x .|. ((a * y) + (b * z)) = (a * (x .|. y)) + (b * (x .|. z))
let x be Point of V; :: thesis: for y, z being Point of (DualSp V)
for a, b being Real holds x .|. ((a * y) + (b * z)) = (a * (x .|. y)) + (b * (x .|. z))
let y, z be Point of (DualSp V); :: thesis: for a, b being Real holds x .|. ((a * y) + (b * z)) = (a * (x .|. y)) + (b * (x .|. z))
let a, b be Real; :: thesis: x .|. ((a * y) + (b * z)) = (a * (x .|. y)) + (b * (x .|. z))
thus x .|. ((a * y) + (b * z)) = (x .|. (a * y)) + (x .|. (b * z)) by DUALSP01:29
.= (a * (x .|. y)) + (x .|. (b * z)) by DUALSP01:30
.= (a * (x .|. y)) + (b * (x .|. z)) by DUALSP01:30 ; :: thesis: verum