deffunc H₁( object ) -> set = W . (p . $1);
consider f being Function such that
A2: ( dom f = dom p & ( for x being object st x in dom p holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();

A3: now :: thesis: for i being Nat st i in dom f holds
f . i in REAL

let i be Nat; :: thesis: ( i in dom f implies f . i in REAL )
A4: W is Function of the carrier' of G,REAL by A1;
assume A5: i in dom f ; :: thesis: f . i in REAL
then f . i = W . (p . i) by A2;
hence f . i in REAL by A2, A5, A4, FINSEQ_2:11, FUNCT_2:5; :: thesis: verum

end;

dom f = Seg (len p) by A2, FINSEQ_1:def 3;
then f is FinSequence by FINSEQ_1:def 2;
then reconsider g = f as FinSequence of REAL by A3, FINSEQ_2:12;
take g ; :: thesis: ( dom p = dom g & ( for i being Nat st i in dom p holds
g . i = W . (p . i) ) )
thus dom p = dom g by A2; :: thesis: for i being Nat st i in dom p holds
g . i = W . (p . i)
let i be Nat; :: thesis: ( i in dom p implies g . i = W . (p . i) )
assume i in dom p ; :: thesis: g . i = W . (p . i)
hence g . i = W . (p . i) by A2; :: thesis: verum