let f be complex-valued Function; :: thesis: (f ") ^2 = (f ^2) "
A1: dom ((f ") ^2) = dom (f ") by VALUED_1:11;
A2: dom (f ") = dom f by VALUED_1:def 7;
dom ((f ^2) ") = dom (f ^2) by VALUED_1:def 7;
hence dom ((f ") ^2) = dom ((f ^2) ") by A1, A2, VALUED_1:11; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 ((f ") ^2) or ((f ") ^2) . b₁ = ((f ^2) ") . b₁ )
let x be object ; :: thesis: ( not x in proj1 ((f ") ^2) or ((f ") ^2) . x = ((f ^2) ") . x )
assume x in dom ((f ") ^2) ; :: thesis: ((f ") ^2) . x = ((f ^2) ") . x
A3: (f ^2) . x = (f . x) ^2 by VALUED_1:11;
(f ") . x = (f . x) " by VALUED_1:10;
hence ((f ") ^2) . x = (1 / (f . x)) ^2 by VALUED_1:11
.= (1 ^2) / ((f . x) ^2) by XCMPLX_1:76
.= ((f ^2) ") . x by A3, VALUED_1:10 ;
:: thesis: verum