let D be non empty set ; :: thesis: for r being Real
for Y being RealNormSpace
for G, H being Functional_Sequence of D, the carrier of Y holds
( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )
let r be Real; :: thesis: for Y being RealNormSpace
for G, H being Functional_Sequence of D, the carrier of Y holds
( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )
let Y be RealNormSpace; :: thesis: for G, H being Functional_Sequence of D, the carrier of Y holds
( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )
let G, H be Functional_Sequence of D, the carrier of Y; :: thesis: ( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) )
now :: thesis: for n being Element of NAT holds (r (#) (G + H)) . n = ((r (#) G) + (r (#) H)) . n
let n be Element of NAT ; :: thesis: (r (#) (G + H)) . n = ((r (#) G) + (r (#) H)) . n
thus (r (#) (G + H)) . n = r (#) ((G + H) . n) by Def1
.= r (#) ((G . n) + (H . n)) by Def5
.= (r (#) (G . n)) + (r (#) (H . n)) by VFUNCT_1:13
.= ((r (#) G) . n) + (r (#) (H . n)) by Def1
.= ((r (#) G) . n) + ((r (#) H) . n) by Def1
.= ((r (#) G) + (r (#) H)) . n by Def5 ; :: thesis: verum
end;
hence r (#) (G + H) = (r (#) G) + (r (#) H) by FUNCT_2:63; :: thesis: r (#) (G - H) = (r (#) G) - (r (#) H)
now :: thesis: for n being Element of NAT holds (r (#) (G - H)) . n = ((r (#) G) - (r (#) H)) . n
let n be Element of NAT ; :: thesis: (r (#) (G - H)) . n = ((r (#) G) - (r (#) H)) . n
thus (r (#) (G - H)) . n = r (#) ((G - H) . n) by Def1
.= r (#) ((G . n) - (H . n)) by Th3
.= (r (#) (G . n)) - (r (#) (H . n)) by VFUNCT_1:15
.= ((r (#) G) . n) - (r (#) (H . n)) by Def1
.= ((r (#) G) . n) - ((r (#) H) . n) by Def1
.= ((r (#) G) - (r (#) H)) . n by Th3 ; :: thesis: verum
end;
hence r (#) (G - H) = (r (#) G) - (r (#) H) by FUNCT_2:63; :: thesis: verum