let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX
for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.|
let f be PartFunc of C,COMPLEX ; :: thesis: for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.|
let r be Element of COMPLEX ; :: thesis: |.(r (#) f).| = |.r.| (#) |.f.|
A1: dom f = dom |.f.| by VALUED_1:def 11;
A2: dom |.(r (#) f).| = dom (r (#) f) by VALUED_1:def 11
.= dom f by Th7
.= dom (|.r.| (#) |.f.|) by A1, VALUED_1:def 5 ;

now

let c be Element of C; :: 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) by VALUED_1:def 11;
A5: c in dom |.f.| by A2, A3, VALUED_1:def 5;
thus |.(r (#) f).| . c = |.((r (#) f) . c).| by VALUED_1:18
.= |.((r (#) f) /. c).| by A4, PARTFUN1:def 8
.= |.(r * (f /. c)).| by A4, Th7
.= |.r.| * |.(f /. c).| by COMPLEX1:151
.= |.r.| * |.(f . c).| by A1, A5, PARTFUN1:def 8
.= |.r.| * (|.f.| . c) by VALUED_1:18
.= (|.r.| (#) |.f.|) . c by A2, A3, VALUED_1:def 5 ; :: thesis: verum

end;

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