deffunc H_{1}( 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_{1}(i)
from FINSEQ_1:sch 2();

rng r c= bool X

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:29;

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

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

rng r c= bool X

proof

then reconsider r = r as FinSequence of bool X by FINSEQ_1:def 4;
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 A1, A3, FINSEQ_1:def 3;

then A6: i in dom p by FINSEQ_1:def 3;

end;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 A1, A3, FINSEQ_1:def 3;

then A6: i in dom p by FINSEQ_1:def 3;

now :: thesis: z in bool Xend;

hence
z in bool X
; :: thesis: verumtake 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:29;

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