let F be real-valued FinSequence; :: thesis: sqr (- F) = sqr F
A1: dom (sqr (- F)) = dom (- F) by VALUED_1:11
.= dom F by VALUED_1:8 ;
A2: dom (sqr F) = dom F by VALUED_1:11;

now :: thesis: for j being Nat st j in dom (sqr (- F)) holds
(sqr (- F)) . j = (sqr F) . j

let j be Nat; :: thesis: ( j in dom (sqr (- F)) implies (sqr (- F)) . j = (sqr F) . j )
assume j in dom (sqr (- F)) ; :: thesis: (sqr (- F)) . j = (sqr F) . j
set r = F . j;
set r9 = (- F) . j;
thus (sqr (- F)) . j = ((- F) . j) ^2 by VALUED_1:11
.= (- (F . j)) ^2 by VALUED_1:8
.= (F . j) ^2
.= (sqr F) . j by VALUED_1:11 ; :: thesis: verum

end;

hence sqr (- F) = sqr F by A1, A2, FINSEQ_1:13; :: thesis: verum