deffunc H₁( set ) -> Element of Z_2 = (s . $1) @ x;
consider p being FinSequence such that
A1: len p = len s and
A2: for k being Nat st k in dom p holds
p . k = H₁(k) from FINSEQ_1:sch 2();
A3: for j being Nat st 1 <= j & j <= len s holds
p . j = (s . j) @ x by A1, FINSEQ_3:25, A2;
rng p c= the carrier of Z_2

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in the carrier of Z_2 )
assume y in rng p ; :: thesis: y in the carrier of Z_2
then consider a being object such that
A4: a in dom p and
A5: p . a = y by FUNCT_1:def 3;
p . a = (s . a) @ x by A2, A4;
hence y in the carrier of Z_2 by A5; :: thesis: verum

end;

then reconsider p = p as FinSequence of Z_2 by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = len s & ( for j being Nat st 1 <= j & j <= len s holds
p . j = (s . j) @ x ) )
thus ( len p = len s & ( for j being Nat st 1 <= j & j <= len s holds
p . j = (s . j) @ x ) ) by A1, A3; :: thesis: verum