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) . b1 = (- (F # x)) . b1
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
.= - ((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) . b1 = (- (F # x)) . b1
hence ((- F) # x) . n = (- (F # x)) . n by ; :: thesis: verum
end;
suppose A5: not x in dom (F . n) ; :: thesis: ((- F) # x) . b1 = (- (F # x)) . b1
then A6: not x in dom (- (F . n)) by MESFUNC1:def 7;
(- (F # x)) . n = - 0 by ;
hence ((- F) # x) . n = (- (F # x)) . n by ; :: thesis: verum
end;
end;
end;
hence (- F) # x = - (F # x) by FUNCT_2:def 8; :: thesis: verum