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