let F1, F2 be complex-valued FinSequence; :: thesis: - (F1 + F2) = (- F1) + (- F2)
A1: dom (- (F1 + F2)) = dom (F1 + F2) by VALUED_1:8;
A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def 1;
A3: dom ((- F1) + (- F2)) = (dom (- F1)) /\ (dom (- F2)) by VALUED_1:def 1
.= (dom F1) /\ (dom (- F2)) by VALUED_1:8
.= (dom F1) /\ (dom F2) by VALUED_1:8 ;

now :: thesis: for i being Nat st i in dom (- (F1 + F2)) holds
(- (F1 + F2)) . i = ((- F1) + (- F2)) . i

let i be Nat; :: thesis: ( i in dom (- (F1 + F2)) implies (- (F1 + F2)) . i = ((- F1) + (- F2)) . i )
assume A4: i in dom (- (F1 + F2)) ; :: thesis: (- (F1 + F2)) . i = ((- F1) + (- F2)) . i
thus (- (F1 + F2)) . i = - ((F1 + F2) . i) by VALUED_1:8
.= - ((F1 . i) + (F2 . i)) by A1, A4, VALUED_1:def 1
.= (- (F1 . i)) + (- (F2 . i))
.= (- (F1 . i)) + ((- F2) . i) by VALUED_1:8
.= ((- F1) . i) + ((- F2) . i) by VALUED_1:8
.= ((- F1) + (- F2)) . i by A1, A2, A3, A4, VALUED_1:def 1 ; :: thesis: verum

end;

hence - (F1 + F2) = (- F1) + (- F2) by A2, A3, FINSEQ_1:13, VALUED_1:8; :: thesis: verum