let X be non empty set ; :: thesis: for F being Functional_Sequence of X,ExtREAL
for x being Element of X holds (- F) # x = - (F # x)
let F be Functional_Sequence of X,ExtREAL; :: thesis: for x being Element of X holds (- F) # x = - (F # x)
let x be Element of X; :: thesis: (- F) # x = - (F # x)

now :: thesis: for n being Element of NAT holds ((- F) # x) . n = (- (F # x)) . n

let n be Element of NAT ; :: thesis: ((- F) # x) . b₁ = (- (F # x)) . b₁
A1: dom (- (F # x)) = NAT by FUNCT_2:def 1;
A2: ((- F) # x) . n = ((- F) . n) . x by MESFUNC5:def 13
.= (- (F . n)) . x by Th37 ;
A3: (- (F # x)) . n = - ((F # x) . n) by A1, MESFUNC1:def 7
.= - ((F . n) . x) by MESFUNC5:def 13 ;
A4: dom (F . n) = dom (- (F . n)) by MESFUNC1:def 7;

per cases ( x in dom (F . n) or not x in dom (F . n) ) ;

suppose x in dom (F . n) ; :: thesis: ((- F) # x) . b₁ = (- (F # x)) . b₁

hence ((- F) # x) . n = (- (F # x)) . n by A3, A2, A4, MESFUNC1:def 7; :: thesis: verum

end;

suppose A5: not x in dom (F . n) ; :: thesis: ((- F) # x) . b₁ = (- (F # x)) . b₁

then A6: not x in dom (- (F . n)) by MESFUNC1:def 7;
(- (F # x)) . n = - 0 by A3, A5, FUNCT_1:def 2;
hence ((- F) # x) . n = (- (F # x)) . n by A6, A2, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence (- F) # x = - (F # x) by FUNCT_2:def 8; :: thesis: verum