let f be complex-valued FinSequence; :: thesis: len (f ^2) = len f
dom (f ^2) = dom f by VALUED_1:11;
hence len (f ^2) = len f by FINSEQ_3:29; :: thesis: verum