let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,the carrier of V
for z being Complex holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,the carrier of V
for z being Complex holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
let f be PartFunc of M,the carrier of V; :: thesis: for z being Complex holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
let z be Complex; :: thesis: ||.(z (#) f).|| = |.z.| (#) ||.f.||
A1: dom ||.(z (#) f).|| = dom (z (#) f) by Def5
.= dom f by Def4
.= dom ||.f.|| by Def5
.= dom (|.z.| (#) ||.f.||) by VALUED_1:def 5 ;

now

let c be Element of M; :: thesis: ( c in dom ||.(z (#) f).|| implies ||.(z (#) f).|| . c = (|.z.| (#) ||.f.||) . c )
assume A2: c in dom ||.(z (#) f).|| ; :: thesis: ||.(z (#) f).|| . c = (|.z.| (#) ||.f.||) . c
then A3: c in dom ||.f.|| by A1, VALUED_1:def 5;
A4: c in dom (z (#) f) by A2, Def5;
thus ||.(z (#) f).|| . c = ||.((z (#) f) /. c).|| by A2, Def5
.= ||.(z * (f /. c)).|| by A4, Def4
.= |.z.| * ||.(f /. c).|| by CLVECT_1:def 11
.= |.z.| * (||.f.|| . c) by A3, Def5
.= (|.z.| (#) ||.f.||) . c by A1, A2, VALUED_1:def 5 ; :: thesis: verum

end;

hence ||.(z (#) f).|| = |.z.| (#) ||.f.|| by A1, PARTFUN1:34; :: thesis: verum