let x, y be Real; :: thesis: for f being real-valued FinSequence holds (x - y) * f = (x * f) - (y * f)
let f be real-valued FinSequence; :: thesis: (x - y) * f = (x * f) - (y * f)
A1: dom ((x - y) * f) = dom f by VALUED_1:def 5;
A2: dom ((x * f) - (y * f)) = (dom (x * f)) /\ (dom (y * f)) by VALUED_1:12;
A3: dom (x * f) = dom f by VALUED_1:def 5;
A4: dom (y * f) = dom f by VALUED_1:def 5;
now :: thesis: for n being Nat st n in dom ((x - y) * f) holds
((x - y) * f) . n = ((x * f) - (y * f)) . n
let n be Nat; :: thesis: ( n in dom ((x - y) * f) implies ((x - y) * f) . n = ((x * f) - (y * f)) . n )
assume A5: n in dom ((x - y) * f) ; :: thesis: ((x - y) * f) . n = ((x * f) - (y * f)) . n
thus ((x - y) * f) . n = (x - y) * (f . n) by VALUED_1:6
.= (x * (f . n)) - (y * (f . n))
.= (x * (f . n)) - ((y * f) . n) by VALUED_1:6
.= ((x * f) . n) - ((y * f) . n) by VALUED_1:6
.= ((x * f) - (y * f)) . n by A1, A2, A3, A4, A5, VALUED_1:13 ; :: thesis: verum
end;
hence (x - y) * f = (x * f) - (y * f) by A1, A2, A3, A4; :: thesis: verum