let y1, y2 be FinSequence of the carrier of R; :: thesis: ( dom y1 = dom p & ( for i being Nat st 1 <= i & i <= len y1 holds
y1 /. i = (p /. i) + (q /. i) ) & dom y2 = dom p & ( for i being Nat st 1 <= i & i <= len y2 holds
y2 /. i = (p /. i) + (q /. i) ) implies y1 = y2 )
assume that
A4: dom y1 = dom p and
A5: for i being Nat st 1 <= i & i <= len y1 holds
y1 /. i = (p /. i) + (q /. i) and
A6: dom y2 = dom p and
A7: for i being Nat st 1 <= i & i <= len y2 holds
y2 /. i = (p /. i) + (q /. i) ; :: thesis: y1 = y2
A8: Seg (len y1) = dom y2 by A4, A6, FINSEQ_1:def 3
.= Seg (len y2) by FINSEQ_1:def 3 ;
then A9: len y1 = len y2 by FINSEQ_1:6;

now :: thesis: for i being Nat st 1 <= i & i <= len y1 holds
y1 . i = y2 . i

let i be Nat; :: thesis: ( 1 <= i & i <= len y1 implies y1 . i = y2 . i )
assume A10: ( 1 <= i & i <= len y1 ) ; :: thesis: y1 . i = y2 . i
then i in Seg (len y2) by A8, FINSEQ_1:1;
then A11: i in dom y2 by FINSEQ_1:def 3;
i in Seg (len y1) by A10, FINSEQ_1:1;
then i in dom y1 by FINSEQ_1:def 3;
hence y1 . i = y1 /. i by PARTFUN1:def 6
.= (p /. i) + (q /. i) by A5, A10
.= y2 /. i by A7, A9, A10
.= y2 . i by A11, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence y1 = y2 by A8, FINSEQ_1:6, FINSEQ_1:14; :: thesis: verum