let i, j be Nat; :: thesis: ( i <= j implies for R1 being i -element complex-valued FinSequence
for R being j -element complex-valued FinSequence holds R1 = (R1 - R) + R )
assume A1: i <= j ; :: thesis: for R1 being i -element complex-valued FinSequence
for R being j -element complex-valued FinSequence holds R1 = (R1 - R) + R
let R1 be i -element complex-valued FinSequence; :: thesis: for R being j -element complex-valued FinSequence holds R1 = (R1 - R) + R
let R be j -element complex-valued FinSequence; :: thesis: R1 = (R1 - R) + R
A2: ( len R1 = i & len R = j ) by CARD_1:def 7;
A4: dom (R1 - R) = (dom R1) /\ (dom R) by VALUED_1:12
.= dom R1 by A2, XBOOLE_1:28, A1, FINSEQ_3:30 ;
A5: dom ((R1 - R) + R) = (dom (R1 - R)) /\ (dom R) by VALUED_1:def 1
.= dom R1 by A2, A4, XBOOLE_1:28, A1, FINSEQ_3:30 ;

now :: thesis: for x being object st x in dom R1 holds
((R1 - R) + R) . x = R1 . x

let x be object ; :: thesis: ( x in dom R1 implies ((R1 - R) + R) . x = R1 . x )
assume A6: x in dom R1 ; :: thesis: ((R1 - R) + R) . x = R1 . x
hence ((R1 - R) + R) . x = ((R1 - R) . x) + (R . x) by A5, VALUED_1:def 1
.= ((R1 . x) - (R . x)) + (R . x) by A4, A6, VALUED_1:13
.= R1 . x ;
:: thesis: verum

end;

hence R1 = (R1 - R) + R by A5, FUNCT_1:def 11; :: thesis: verum