let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for n being Nat holds (- F) . n = - (F . n)
let F be Functional_Sequence of X,ExtREAL; :: thesis: for n being Nat holds (- F) . n = - (F . n)
let n be Nat; :: thesis: (- F) . n = - (F . n)
thus (- F) . n = (- 1) (#) (F . n) by Def1
.= - (F . n) by MESFUNC2:9 ; :: thesis: verum