deffunc H_{1}( 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_{1}(i) ) )
from FINSEQ_1:sch 2();

rng G c= the carrier of F_Real

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

consider G being FinSequence such that

A1: ( len G = len F & ( for i being Nat st i in dom G holds

G . i = H

rng G c= the carrier of F_Real

proof

then reconsider G = G as FinSequence of F_Real by FINSEQ_1:def 4;
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;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

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