deffunc H₁( object ) -> Element of the carrier of F_Real = (ScProductDM L) . (v,((f . (F /. $1)) * (F /. $1)));
consider G being FinSequence such that
A1: ( len G = len F & ( for i being Nat st i in dom G holds
G . i = H₁(i) ) ) from FINSEQ_1:sch 2();
rng G c= the carrier of F_Real

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng G or x in the carrier of F_Real )
assume B1: x in rng G ; :: thesis: x in the carrier of F_Real
consider z being object such that
B2: ( z in dom G & x = G . z ) by B1, FUNCT_1:def 3;
x = (ScProductDM L) . (v,((f . (F /. z)) * (F /. z))) by A1, B2;
hence x in the carrier of F_Real ; :: thesis: verum

end;

then reconsider G = G as FinSequence of F_Real by FINSEQ_1:def 4;
take G ; :: thesis: ( len G = len F & ( for i being Nat st i in dom G holds
G . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) )
thus ( len G = len F & ( for i being Nat st i in dom G holds
G . i = (ScProductDM L) . (v,((f . (F /. i)) * (F /. i))) ) ) by A1; :: thesis: verum