let x, y be real number ; :: thesis: for n being Element of NAT
for f being Element of n -tuples_on REAL holds (x - y) * f = (x * f) - (y * f)
let n be Element of NAT ; :: thesis: for f being Element of n -tuples_on REAL holds (x - y) * f = (x * f) - (y * f)
let f be Element of n -tuples_on REAL ; :: thesis: (x - y) * f = (x * f) - (y * f)
REAL n = n -tuples_on REAL by EUCLID:def 1;
then reconsider g = f as Point of (TOP-REAL n) by EUCLID:25;
(x - y) * g = (x * g) - (y * g) by EUCLID:54;
hence (x - y) * f = (x * f) - (y * f) ; :: thesis: verum