let X be ComplexUnitarySpace; :: thesis: for p, q being Complex
for x, y being Point of X holds ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((p *') * q) * (y .|. x))) + ((q * (q *')) * (y .|. y))
let p, q be Complex; :: thesis: for x, y being Point of X holds ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((p *') * q) * (y .|. x))) + ((q * (q *')) * (y .|. y))
let x, y be Point of X; :: thesis: ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((p *') * q) * (y .|. x))) + ((q * (q *')) * (y .|. y))
((p * x) + (q * y)) .|. ((p * x) + (q * y)) = (p * (x .|. ((p * x) + (q * y)))) + (q * (y .|. ((p * x) + (q * y)))) by Th22
.= (p * (((p *') * (x .|. x)) + ((q *') * (x .|. y)))) + (q * (y .|. ((p * x) + (q * y)))) by Th23
.= (((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (q * (((p *') * (y .|. x)) + ((q *') * (y .|. y)))) by Th23
.= (((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((q * (p *')) * (y .|. x)) + ((q * (q *')) * (y .|. y))) ;
hence ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *')) * (x .|. x)) + ((p * (q *')) * (x .|. y))) + (((p *') * q) * (y .|. x))) + ((q * (q *')) * (y .|. y)) ; :: thesis: verum