let t be Real; :: 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

thus (f + (NAT --> t)) . n = (f . n) + ((NAT --> t) . n) by VALUED_1:1

.= (f + t) . n by VALUED_1:2 ; :: thesis: verum

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

thus (f + (NAT --> t)) . n = (f . n) + ((NAT --> t) . n) by VALUED_1:1

.= (f + t) . n by VALUED_1:2 ; :: thesis: verum