theorem :: ANPROJ10:36

for a being Real
for p being Tuple of 1, REAL holds multreal .: (((dom p) --> a),p) = a * p by Th22;