let f be complex-valued Function; :: thesis: ( dom (f ^2) = dom f & ( for c being object holds (f ^2) . c = (f . c) ^2 ) )
thus A1: dom (f ^2) = (dom f) /\ (dom f) by Def4
.= dom f ; :: thesis: for c being object holds (f ^2) . c = (f . c) ^2
let c be object ; :: thesis: (f ^2) . c = (f . c) ^2

per cases ( c in dom f or not c in dom f ) ;

suppose c in dom f ; :: thesis: (f ^2) . c = (f . c) ^2

hence (f ^2) . c = (f . c) ^2 by A1, Def4; :: thesis: verum

end;

suppose A2: not c in dom f ; :: thesis: (f ^2) . c = (f . c) ^2

hence (f ^2) . c = 0 ^2 by A1, FUNCT_1:def 2
.= (f . c) ^2 by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;