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

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))) ; :: thesis: r1 = r2

A11: dom r1 = Seg (len p) by A7, FINSEQ_1:def 3;

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))) ; :: thesis: r1 = r2

A11: dom r1 = Seg (len p) by A7, FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom r1 holds

r1 . i = r2 . i

hence
r1 = r2
by A7, A9, FINSEQ_2:9; :: thesis: verumr1 . i = r2 . i

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 A11, FINSEQ_1:def 3;

hence r1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by A8

.= r2 . i by A10, A12 ;

:: thesis: verum

end;assume i in dom r1 ; :: thesis: r1 . i = r2 . i

then A12: i in dom p by A11, FINSEQ_1:def 3;

hence r1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) by A8

.= r2 . i by A10, A12 ;

:: thesis: verum