let r1, r2 be Real; :: thesis: for F being real-valued FinSequence holds (r1 + r2) * F = (r1 * F) + (r2 * F)
let F be real-valued FinSequence; :: thesis: (r1 + r2) * F = (r1 * F) + (r2 * F)
A1: dom ((r1 + r2) * F) = dom F by VALUED_1:def 5;
A2: dom ((r1 * F) + (r2 * F)) = (dom (r1 * F)) /\ (dom (r2 * F)) by VALUED_1:def 1;
A3: dom (r1 * F) = dom F by VALUED_1:def 5;
A4: dom (r2 * F) = dom F by VALUED_1:def 5;

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

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

end;

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