let f be complex-valued Function; :: thesis: for r being Complex st r <> 0 holds

(r (#) f) ^ = (r ") (#) (f ^)

let r be Complex; :: thesis: ( r <> 0 implies (r (#) f) ^ = (r ") (#) (f ^) )

assume A1: r <> 0 ; :: thesis: (r (#) f) ^ = (r ") (#) (f ^)

A2: dom ((r (#) f) ^) = (dom (r (#) f)) \ ((r (#) f) " {0}) by Def2

.= (dom (r (#) f)) \ (f " {0}) by A1, Th7

.= (dom f) \ (f " {0}) by VALUED_1:def 5

.= dom (f ^) by Def2

.= dom ((r ") (#) (f ^)) by VALUED_1:def 5 ;

(r (#) f) ^ = (r ") (#) (f ^)

let r be Complex; :: thesis: ( r <> 0 implies (r (#) f) ^ = (r ") (#) (f ^) )

assume A1: r <> 0 ; :: thesis: (r (#) f) ^ = (r ") (#) (f ^)

A2: dom ((r (#) f) ^) = (dom (r (#) f)) \ ((r (#) f) " {0}) by Def2

.= (dom (r (#) f)) \ (f " {0}) by A1, Th7

.= (dom f) \ (f " {0}) by VALUED_1:def 5

.= dom (f ^) by Def2

.= dom ((r ") (#) (f ^)) by VALUED_1:def 5 ;

now :: thesis: for c being object st c in dom ((r (#) f) ^) holds

((r (#) f) ^) . c = ((r ") (#) (f ^)) . c

hence
(r (#) f) ^ = (r ") (#) (f ^)
by A2, FUNCT_1:2; :: thesis: verum((r (#) f) ^) . c = ((r ") (#) (f ^)) . c

let c be object ; :: thesis: ( c in dom ((r (#) f) ^) implies ((r (#) f) ^) . c = ((r ") (#) (f ^)) . c )

assume A3: c in dom ((r (#) f) ^) ; :: thesis: ((r (#) f) ^) . c = ((r ") (#) (f ^)) . c

then A4: c in (dom (r (#) f)) \ ((r (#) f) " {0}) by Def2;

A5: c in dom (f ^) by A2, A3, VALUED_1:def 5;

thus ((r (#) f) ^) . c = ((r (#) f) . c) " by A3, Def2

.= (r * (f . c)) " by A4, VALUED_1:def 5

.= (r ") * ((f . c) ") by XCMPLX_1:204

.= (r ") * ((f ^) . c) by A5, Def2

.= ((r ") (#) (f ^)) . c by A2, A3, VALUED_1:def 5 ; :: thesis: verum

end;assume A3: c in dom ((r (#) f) ^) ; :: thesis: ((r (#) f) ^) . c = ((r ") (#) (f ^)) . c

then A4: c in (dom (r (#) f)) \ ((r (#) f) " {0}) by Def2;

A5: c in dom (f ^) by A2, A3, VALUED_1:def 5;

thus ((r (#) f) ^) . c = ((r (#) f) . c) " by A3, Def2

.= (r * (f . c)) " by A4, VALUED_1:def 5

.= (r ") * ((f . c) ") by XCMPLX_1:204

.= (r ") * ((f ^) . c) by A5, Def2

.= ((r ") (#) (f ^)) . c by A2, A3, VALUED_1:def 5 ; :: thesis: verum