let i be Nat; :: thesis: for R being Element of i -tuples_on REAL holds sqr (- R) = sqr R
let R be Element of i -tuples_on REAL ; :: thesis: sqr (- R) = sqr R

now

let j be Nat; :: thesis: ( j in Seg i implies (sqr (- R)) . j = (sqr R) . j )
assume j in Seg i ; :: thesis: (sqr (- R)) . j = (sqr R) . j
set r = R . j;
set r' = (- R) . j;
thus (sqr (- R)) . j = ((- R) . j) ^2 by VALUED_1:11
.= (- (R . j)) ^2 by Th35
.= (R . j) ^2
.= (sqr R) . j by VALUED_1:11 ; :: thesis: verum

end;

hence sqr (- R) = sqr R by FINSEQ_2:139; :: thesis: verum