let a, b be Complex; :: thesis: for X being ComplexUnitarySpace
for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))
let X be ComplexUnitarySpace; :: thesis: for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))
let x, y, z be Point of X; :: thesis: ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))
((a * x) + (b * y)) .|. z = ((a * x) .|. z) + ((b * y) .|. z) by Def11
.= (a * (x .|. z)) + ((b * y) .|. z) by Def11 ;
hence ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z)) by Def11; :: thesis: verum