deffunc H_{1}( 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_{1}(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

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

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