let c be Complex; :: thesis: for f being complex-valued FinSequence holds (f (/) c) ^2 = (f ^2) (/) (c ^2)
let f be complex-valued FinSequence; :: thesis: (f (/) c) ^2 = (f ^2) (/) (c ^2)
thus (f (/) c) ^2 = ((1 / c) ^2) (#) (f ^2) by Th17
.= ((1 * 1) / (c * c)) (#) (f ^2) by XCMPLX_1:76
.= (f ^2) (/) (c ^2) ; :: thesis: verum