let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for z being Complex holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for z being Complex holds ||.(z (#) f).|| = |.z.| (#) ||.f.||
let f be PartFunc of M,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 NORMSP_0:def 3
.= dom f by Def2
.= dom ||.f.|| by NORMSP_0:def 3
.= dom (|.z.| (#) ||.f.||) by VALUED_1:def 5 ;
now :: thesis: for c being Element of M st c in dom ||.(z (#) f).|| holds
||.(z (#) f).|| . c = (|.z.| (#) ||.f.||) . c
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, NORMSP_0:def 3;
thus ||.(z (#) f).|| . c = ||.((z (#) f) /. c).|| by A2, NORMSP_0:def 3
.= ||.(z * (f /. c)).|| by A4, Def2
.= |.z.| * ||.(f /. c).|| by CLVECT_1:def 13
.= |.z.| * (||.f.|| . c) by A3, NORMSP_0:def 3
.= (|.z.| (#) ||.f.||) . c by A1, A2, VALUED_1:def 5 ; :: thesis: verum
end;
hence ||.(z (#) f).|| = |.z.| (#) ||.f.|| by A1, PARTFUN1:5; :: thesis: verum