let c be Complex; :: 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 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom ((f (/) c) ^2) or ((f (/) c) ^2) . b_{1} = ((f ^2) (/) (c ^2)) . b_{1} )

let x be object ; :: thesis: ( not x in dom ((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:76

.= ((f ^2) . x) / (c ^2) by VALUED_1:11

.= ((f ^2) (/) (c ^2)) . x by VALUED_2:29 ; :: thesis: verum

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 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom ((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:76

.= ((f ^2) . x) / (c ^2) by VALUED_1:11

.= ((f ^2) (/) (c ^2)) . x by VALUED_2:29 ; :: thesis: verum