deffunc H₁( Nat) -> Element of omega = primenumber $1;
consider f being Real_Sequence such that
A1: for i being Nat holds f . i = H₁(i) from SEQ_1:sch 1();
reconsider f = f as Function of NAT,REAL ;
A3: for n being Nat holds f . n is Element of NAT

proof

let n be Nat; :: thesis: f . n is Element of NAT
f . n = primenumber n by A1;
hence f . n is Element of NAT ; :: thesis: verum

end;

for n, m being Nat st n < m holds
f . n < f . m

proof

let n, m be Nat; :: thesis: ( n < m implies f . n < f . m )
assume C1: n < m ; :: thesis: f . n < f . m
( f . n = primenumber n & f . m = primenumber m ) by A1;
hence f . n < f . m by Cosik1, C1; :: thesis: verum

end;

then reconsider f = f as increasing sequence of NAT by A3, SEQM_3:13, SEQM_3:1;
take f ; :: according to VALUED_0:def 17 :: thesis: ReciPrime = f * invNAT
ReciPrime = invNAT * f

proof

for x being Element of NAT holds ReciPrime . x = (invNAT * f) . x

proof

let x be Element of NAT ; :: thesis: ReciPrime . x = (invNAT * f) . x
dom f = NAT by FUNCT_2:def 1;
then (invNAT * f) . x = invNAT . (f . x) by FUNCT_1:13
.= invNAT . (primenumber x) by A1
.= 1 / (primenumber x) by DefRec ;
hence ReciPrime . x = (invNAT * f) . x by ReciPr; :: thesis: verum

end;

hence ReciPrime = invNAT * f by FUNCT_2:def 8; :: thesis: verum

end;

hence ReciPrime = f * invNAT ; :: thesis: verum