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

end;

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