deffunc H₁( Nat) -> set = IFEQ (q . $1),TRUE ,(p . $1),(X \ (p . $1));
consider r being FinSequence such that
A1: len r = len p and
A2: for i being Nat st i in dom r holds
r . i = H₁(i) from FINSEQ_1:sch 2();
rng r c= bool X

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng r or z in bool X )
assume z in rng r ; :: thesis: z in bool X
then consider i being Nat such that
A3: i in dom r and
A4: r . i = z by FINSEQ_2:11;
A5: z = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) by A2, A3, A4;
i in Seg (len p) by A1, A3, FINSEQ_1:def 3;
then A6: i in dom p by FINSEQ_1:def 3;

now

per cases ( q . i = TRUE or q . i <> TRUE ) ;

suppose q . i = TRUE ; :: thesis: z in bool X

then z = p . i by A5, FUNCOP_1:def 8;
hence z in bool X by A6, FINSEQ_2:13; :: thesis: verum

end;

suppose q . i <> TRUE ; :: thesis: z in bool X

then z = X \ (p . i) by A5, FUNCOP_1:def 8;
hence z in bool X ; :: thesis: verum

end;

end;

end;

hence z in bool X ; :: thesis: verum

end;

then reconsider r = r as FinSequence of bool X by FINSEQ_1:def 4;
take r ; :: thesis: ( len r = len p & ( for i being Nat st i in dom p holds
r . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) )
dom p = dom r by A1, FINSEQ_3:31;
hence ( len r = len p & ( for i being Nat st i in dom p holds
r . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) ) by A1, A2; :: thesis: verum