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

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