consider p0 being FinSequence such that
A1: rng p0 = Y and
A2: p0 is one-to-one by FINSEQ_4:58;
reconsider p = p0 as FinSequence of the carrier of X by A1, FINSEQ_1:def 4;
set ll = len p;
deffunc H₁( Nat) -> set = PO ($1,p,x);
consider q0 being FinSequence such that
A3: ( len q0 = len p & ( for i being Nat st i in dom q0 holds
q0 . i = H₁(i) ) ) from FINSEQ_1:sch 2();
A4: dom q0 = Seg (len p) by A3, FINSEQ_1:def 3;
A5: dom q0 = dom p by A3, FINSEQ_3:29;

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

let i be Nat; :: thesis: ( i in dom q0 implies q0 . i in REAL )
assume A6: i in dom q0 ; :: thesis: q0 . i in REAL
then A7: q0 . i = PO (i,p,x) by A3
.= the scalar of X . [x,(p . i)] ;
reconsider y = p . i as Point of X by A5, A6, FINSEQ_2:11;
the scalar of X . [x,(p . i)] = x .|. y by BHSP_1:def 1;
hence q0 . i in REAL by A7, XREAL_0:def 1; :: thesis: verum

end;

then reconsider q = q0 as FinSequence of REAL by FINSEQ_2:12;
take addreal "**" q ; :: thesis: ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Nat st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q ) )
take p ; :: thesis: ( p is one-to-one & rng p = Y & ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Nat st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q ) )
thus ( p is one-to-one & rng p = Y ) by A1, A2; :: thesis: ex q being FinSequence of REAL st
( dom q = dom p & ( for i being Nat st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q )
take q ; :: thesis: ( dom q = dom p & ( for i being Nat st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q )
thus ( dom q = dom p & ( for i being Nat st i in dom q holds
q . i = PO (i,p,x) ) & addreal "**" q = addreal "**" q ) by A3, A4, FINSEQ_1:def 3; :: thesis: verum