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

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

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

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

then reconsider p = p as FinSequence of Z_2 by FINSEQ_1:def 4;
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;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

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