deffunc H₁( Nat) -> Element of the carrier of V = (r /. $1) * (x /. $1);
consider z being FinSequence of V such that
A1: ( len z = len x & ( for j being Nat st j in dom z holds
z . j = H₁(j) ) ) from FINSEQ_2:sch 1();
take z ; :: thesis: ( len z = len x & ( for i being Nat st 1 <= i & i <= len x holds
z . i = (r /. i) * (x /. i) ) )
thus ( len z = len x & ( for i being Nat st 1 <= i & i <= len x holds
z . i = (r /. i) * (x /. i) ) ) by A1, FINSEQ_3:25; :: thesis: verum