let G, H be Functional_Sequence of D,REAL; :: thesis: ( ( for n being Nat holds G . n = - (H . n) ) implies for n being Nat holds H . n = - (G . n) )
assume A5: for n being Nat holds G . n = - (H . n) ; :: thesis: for n being Nat holds H . n = - (G . n)
let n be Nat; :: thesis: H . n = - (G . n)
thus H . n = - (- (H . n))
.= - (G . n) by A5 ; :: thesis: verum