let c1, c2 be Complex; :: thesis: for F being complex-valued FinSequence holds (c1 + c2) * F = (c1 * F) + (c2 * F)
let F be complex-valued FinSequence; :: thesis: (c1 + c2) * F = (c1 * F) + (c2 * F)
A1: dom ((c1 + c2) * F) = dom F by VALUED_1:def 5;
A2: dom ((c1 * F) + (c2 * F)) = (dom (c1 * F)) /\ (dom (c2 * F)) by VALUED_1:def 1;
A3: dom (c1 * F) = dom F by VALUED_1:def 5;
A4: dom (c2 * F) = dom F by VALUED_1:def 5;

now :: thesis: for i being Nat st i in dom ((c1 + c2) * F) holds
((c1 + c2) * F) . i = ((c1 * F) + (c2 * F)) . i

let i be Nat; :: thesis: ( i in dom ((c1 + c2) * F) implies ((c1 + c2) * F) . i = ((c1 * F) + (c2 * F)) . i )
assume A5: i in dom ((c1 + c2) * F) ; :: thesis: ((c1 + c2) * F) . i = ((c1 * F) + (c2 * F)) . i
thus ((c1 + c2) * F) . i = (c1 + c2) * (F . i) by VALUED_1:6
.= (c1 * (F . i)) + (c2 * (F . i))
.= (c1 * (F . i)) + ((c2 * F) . i) by VALUED_1:6
.= ((c1 * F) . i) + ((c2 * F) . i) by VALUED_1:6
.= ((c1 * F) + (c2 * F)) . i by A1, A2, A3, A4, A5, VALUED_1:def 1 ; :: thesis: verum

end;

hence (c1 + c2) * F = (c1 * F) + (c2 * F) by A1, A2, A3, A4, FINSEQ_1:13; :: thesis: verum