let D be non empty set ; :: thesis: for G, H, H1 being Functional_Sequence of D,REAL holds
( H1 = G - H iff for n being Nat holds H1 . n = (G . n) - (H . n) )
let G, H, H1 be Functional_Sequence of D,REAL; :: thesis: ( H1 = G - H iff for n being Nat holds H1 . n = (G . n) - (H . n) )
thus ( H1 = G - H implies for n being Nat holds H1 . n = (G . n) - (H . n) ) :: thesis: ( ( for n being Nat holds H1 . n = (G . n) - (H . n) ) implies H1 = G - H )

proof

assume A1: H1 = G - H ; :: thesis: for n being Nat holds H1 . n = (G . n) - (H . n)
let n be Nat; :: thesis: H1 . n = (G . n) - (H . n)
thus H1 . n = (G . n) + ((- H) . n) by A1, Def5
.= (G . n) - (H . n) by Def3 ; :: thesis: verum

end;

assume A2: for n being Nat holds H1 . n = (G . n) - (H . n) ; :: thesis: H1 = G - H

now :: thesis: for n being Element of NAT holds H1 . n = (G - H) . n

let n be Element of NAT ; :: thesis: H1 . n = (G - H) . n
thus H1 . n = (G . n) - (H . n) by A2
.= (G . n) + ((- H) . n) by Def3
.= (G - H) . n by Def5 ; :: thesis: verum

end;

hence H1 = G - H by FUNCT_2:63; :: thesis: verum