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, Def7
.= (G . n) (#) ((H . n) ^) by Def2
.= (G . n) / (H . n) by RFUNCT_1:31 ; :: 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 RFUNCT_1:31
.= (G . n) (#) ((H ") . n) by Def2
.= (G / H) . n by Def7 ; :: thesis: verum

end;

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