deffunc H1( 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 = H1(i) from rng r c= bool X
proof
let z be object ; :: 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:10;
A5: z = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by A2, A3, A4;
i in Seg (len p) by ;
then A6: i in dom p by FINSEQ_1:def 3;
now :: thesis: z in bool X
per cases ( q . i = TRUE or q . i <> TRUE ) ;
suppose q . i = TRUE ; :: thesis: z in bool X
then z = p . i by ;
hence z in bool X by ; :: thesis: verum
end;
suppose q . i <> TRUE ; :: thesis: z in bool X
then z = X \ (p . i) by ;
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 ;
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