deffunc H₁( Nat of n) -> Element of the carrier of the algebra of W = W . (a,(p . $1));
consider z being FinSequence of the carrier of the algebra of W 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),W by A1, FINSEQ_2:92;
take z ; :: thesis: for m being Nat of n holds z . m = W . (a,(p . m))
thus for m being Nat of n holds z . m = W . (a,(p . m)) by A2; :: thesis: verum