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