let f be real-valued FinSequence; :: thesis: sqr (abs f) = sqr f
set n = len f;
reconsider x = f as Element of REAL (len f) by Lm1;

now :: thesis: for k being Nat st k in Seg (len f) holds
(sqr (abs x)) . k = (sqr x) . k

let k be Nat; :: thesis: ( k in Seg (len f) implies (sqr (abs x)) . k = (sqr x) . k )
assume k in Seg (len f) ; :: thesis: (sqr (abs x)) . k = (sqr x) . k
thus (sqr (abs x)) . k = ((abs x) . k) ^2 by VALUED_1:11
.= |.(x . k).| ^2 by VALUED_1:18
.= (x . k) ^2 by COMPLEX1:75
.= (sqr x) . k by VALUED_1:11 ; :: thesis: verum

end;

hence sqr (abs f) = sqr f by FINSEQ_2:119; :: thesis: verum