:: deftheorem defines ^2 VALUED_1:def 8 :
for f being complex-valued Function holds f ^2 = f (#) f;