:: deftheorem Def5 defines #Q PREPOWER:def 6 :
for a being Real
for s being Rational_Sequence
for b₃ being Real_Sequence holds
( b₃ = a #Q s iff for n being Nat holds b₃ . n = a #Q (s . n) );