let t be real number ; :: thesis: for f being Real_Sequence holds f + (NAT --> t) = t + f
let f be Real_Sequence; :: thesis: f + (NAT --> t) = t + f
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (f + (NAT --> t)) . n = (t + f) . n
A1: (NAT --> t) . n = t by FUNCOP_1:7;
thus (f + (NAT --> t)) . n = (f . n) + ((NAT --> t) . n) by VALUED_1:1
.= (f + t) . n by A1, VALUED_1:2 ; :: thesis: verum