deffunc H₁( Nat) -> Element of NAT = DigitDC2 x,$1,k;
consider z being FinSequence of NAT such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H₁(j) from FINSEQ_2:sch 1();
A3: dom z = Seg n by A1, FINSEQ_1:def 3;
reconsider z = z as Tuple of n, NAT by A1, FINSEQ_1:def 18;
take z ; :: thesis: for i being Nat st i in Seg n holds
z . i = DigitDC2 x,i,k
let i be Nat; :: thesis: ( i in Seg n implies z . i = DigitDC2 x,i,k )
assume i in Seg n ; :: thesis: z . i = DigitDC2 x,i,k
hence z . i = DigitDC2 x,i,k by A2, A3; :: thesis: verum