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;
now :: thesis: for i being Nat st i in dom r1 holds
r1 . 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;
hence r1 = r2 by A7, A9, FINSEQ_2:9; :: thesis: verum