let c be complex number ; :: thesis: for f being complex-valued Function holds (f (/) c) ^2 = (f ^2 ) (/) (c ^2 )
let f be complex-valued Function; :: thesis: (f (/) c) ^2 = (f ^2 ) (/) (c ^2 )
thus dom ((f (/) c) ^2 ) = dom (f (/) c) by VALUED_1:11
.= dom f by VALUED_2:28
.= dom (f ^2 ) by VALUED_1:11
.= dom ((f ^2 ) (/) (c ^2 )) by VALUED_2:28 ; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 ((f (/) c) ^2 ) or ((f (/) c) ^2 ) . b₁ = ((f ^2 ) (/) (c ^2 )) . b₁ )
let x be set ; :: thesis: ( not x in proj1 ((f (/) c) ^2 ) or ((f (/) c) ^2 ) . x = ((f ^2 ) (/) (c ^2 )) . x )
assume x in dom ((f (/) c) ^2 ) ; :: thesis: ((f (/) c) ^2 ) . x = ((f ^2 ) (/) (c ^2 )) . x
thus ((f (/) c) ^2 ) . x = ((f (/) c) . x) ^2 by VALUED_1:11
.= ((f . x) / c) ^2 by VALUED_2:29
.= ((f . x) ^2 ) / (c ^2 ) by XCMPLX_1:77
.= ((f ^2 ) . x) / (c ^2 ) by VALUED_1:11
.= ((f ^2 ) (/) (c ^2 )) . x by VALUED_2:29 ; :: thesis: verum