:: deftheorem Def2 defines sqrreal RVSUM_1:def 2 :
for b₁ being UnOp of REAL holds
( b₁ = sqrreal iff for r being Real holds b₁ . r = r ^2 );