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

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

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