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 Lm2;

now

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
.= (abs (x . k)) ^2 by Th6
.= (x . k) ^2 by COMPLEX1:161
.= (sqr x) . k by VALUED_1:11 ; :: thesis: verum

end;

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