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

proof

assume A1: H1 = G / H ; :: thesis: for n being Element of NAT holds H1 . n = (G . n) / (H . n)
let n be Element of NAT ; :: thesis: H1 . n = (G . n) / (H . n)
thus H1 . n = (G . n) (#) ((H ") . n) by A1, Def8
.= (G . n) (#) ((H . n) ^) by Def3
.= (G . n) / (H . n) by RFUNCT_1:31 ; :: thesis: verum

end;

assume A2: for n being Element of NAT holds H1 . n = (G . n) / (H . n) ; :: thesis: H1 = G / H

now

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 Def3
.= (G / H) . n by Def8 ; :: thesis: verum

end;

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