deffunc H₁( Nat) -> Element of K19(K20(D,REAL)) = chi ((f . $1),D);
consider p being FinSequence such that
A1: len p = len f and
A2: for n being Nat st n in dom p holds
p . n = H₁(n) from FINSEQ_1:sch 2();
rng p c= PFuncs (D,REAL)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in PFuncs (D,REAL) )
assume x in rng p ; :: thesis: x in PFuncs (D,REAL)
then consider n being Nat such that
A3: ( n in dom p & p . n = x ) by FINSEQ_2:10;
x = chi ((f . n),D) by A2, A3;
hence x in PFuncs (D,REAL) by PARTFUN1:45; :: thesis: verum

end;

then reconsider p = p as FinSequence of PFuncs (D,REAL) by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = len f & ( for n being Nat st n in dom p holds
p . n = chi ((f . n),D) ) )
thus len p = len f by A1; :: thesis: for n being Nat st n in dom p holds
p . n = chi ((f . n),D)
let n be Nat; :: thesis: ( n in dom p implies p . n = chi ((f . n),D) )
assume n in dom p ; :: thesis: p . n = chi ((f . n),D)
hence p . n = chi ((f . n),D) by A2; :: thesis: verum