let r1, r2 be FinSequence of bool X; ( 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
A7:
len r1 = len p
and
A8:
for i being Nat st i in dom p holds
r1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i)))
and
A9:
len r2 = len p
and
A10:
for i being Nat st i in dom p holds
r2 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i)))
; r1 = r2
A11:
dom r1 = Seg (len p)
by A7, FINSEQ_1:def 3;
hence
r1 = r2
by A7, A9, FINSEQ_2:9; verum