let c be Complex; :: thesis: for f being complex-valued FinSequence holds (c (#) f) ^2 = (c ^2) (#) (f ^2)
let f be complex-valued FinSequence; :: thesis: (c (#) f) ^2 = (c ^2) (#) (f ^2)
A1: dom ((c (#) f) ^2) = dom (c (#) f) by VALUED_1:11
.= dom f by VALUED_1:def 5 ;
A2: dom ((c ^2) (#) (f ^2)) = dom (f ^2) by VALUED_1:def 5
.= dom f by VALUED_1:11 ;
now :: thesis: for x being object st x in dom ((c (#) f) ^2) holds
((c (#) f) ^2) . x = ((c ^2) (#) (f ^2)) . x
let x be object ; :: thesis: ( x in dom ((c (#) f) ^2) implies ((c (#) f) ^2) . x = ((c ^2) (#) (f ^2)) . x )
assume x in dom ((c (#) f) ^2) ; :: thesis: ((c (#) f) ^2) . x = ((c ^2) (#) (f ^2)) . x
thus ((c (#) f) ^2) . x = ((c (#) f) . x) ^2 by VALUED_1:11
.= (c * (f . x)) ^2 by VALUED_1:6
.= (c ^2) * ((f . x) ^2)
.= (c ^2) * ((f ^2) . x) by VALUED_1:11
.= ((c ^2) (#) (f ^2)) . x by VALUED_1:6 ; :: thesis: verum
end;
hence (c (#) f) ^2 = (c ^2) (#) (f ^2) by A1, A2; :: thesis: verum