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:92;
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