theorem Th11: :: VALUED_1:11

for f being complex-valued Function holds
( dom (f ^2) = dom f & ( for c being object holds (f ^2) . c = (f . c) ^2 ) )