deffunc H₁( Nat of n) -> Element of the carrier of RAS = a,(x . $1) . W;
consider z being FinSequence of the carrier of RAS such that
A1: len z = n + 1 and
A2: for m being Nat of n holds z . m = H₁(m) from MIDSP_3:sch 1();
reconsider z = z as Tuple of (n + 1),RAS by A1, FINSEQ_2:110;
take z ; :: thesis: for m being Nat of n holds z . m = a,(x . m) . W
thus for m being Nat of n holds z . m = a,(x . m) . W by A2; :: thesis: verum