let r1, r2 be FinSequence of bool X; :: thesis: ( len r1 = len p & ( for i being Nat st i in dom p holds
r1 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) & len r2 = len p & ( for i being Nat st i in dom p holds
r2 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ) implies r1 = r2 )
assume that
A8: len r1 = len p and
A9: for i being Nat st i in dom p holds
r1 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) and
A10: len r2 = len p and
A11: for i being Nat st i in dom p holds
r2 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) ; :: thesis: r1 = r2
X: dom r1 = Seg (len p) by A8, FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom r1 implies r1 . i = r2 . i )
assume i in dom r1 ; :: thesis: r1 . i = r2 . i
then A12: i in dom p by X, FINSEQ_1:def 3;
hence r1 . i = IFEQ (q . i),TRUE ,(p . i),(X \ (p . i)) by A9
.= r2 . i by A11, A12 ;
:: thesis: verum

end;

hence r1 = r2 by A8, A10, FINSEQ_2:10; :: thesis: verum