let X, Y, W be RealNormSpace; :: thesis: for I being Function of X,Y
for f being PartFunc of Y,W
for r being Real holds r (#) (f * I) = (r (#) f) * I
let I be Function of X,Y; :: thesis: for f being PartFunc of Y,W
for r being Real holds r (#) (f * I) = (r (#) f) * I
let f be PartFunc of Y,W; :: thesis: for r being Real holds r (#) (f * I) = (r (#) f) * I
let r be Real; :: thesis: r (#) (f * I) = (r (#) f) * I
set DI = the carrier of X;
A1: dom (r (#) f) = dom f by VFUNCT_1:def 4;
A2: dom (r (#) (f * I)) = dom (f * I) by VFUNCT_1:def 4;
A3: dom I = the carrier of X by FUNCT_2:def 1;
A4b: for s being Element of the carrier of X holds
( s in dom ((r (#) f) * I) iff s in dom (f * I) )

proof

let s be Element of the carrier of X; :: thesis: ( s in dom ((r (#) f) * I) iff s in dom (f * I) )
( s in dom ((r (#) f) * I) iff I . s in dom (r (#) f) ) by A3, FUNCT_1:11;
hence ( s in dom ((r (#) f) * I) iff s in dom (f * I) ) by A1, A3, FUNCT_1:11; :: thesis: verum

end;

then A4: for s being object holds
( s in dom (r (#) (f * I)) iff s in dom ((r (#) f) * I) ) by A2;
then A4a: dom (r (#) (f * I)) = dom ((r (#) f) * I) by TARSKI:2;
A5: for s being Element of the carrier of X holds
( s in dom ((r (#) f) * I) iff I . s in dom (r (#) f) )

proof

let s be Element of the carrier of X; :: thesis: ( s in dom ((r (#) f) * I) iff I . s in dom (r (#) f) )
dom I = the carrier of X by FUNCT_2:def 1;
hence ( s in dom ((r (#) f) * I) iff I . s in dom (r (#) f) ) by FUNCT_1:11; :: thesis: verum

end;

for z being Element of the carrier of X st z in dom (r (#) (f * I)) holds
(r (#) (f * I)) . z = ((r (#) f) * I) . z

proof

let z be Element of the carrier of X; :: thesis: ( z in dom (r (#) (f * I)) implies (r (#) (f * I)) . z = ((r (#) f) * I) . z )
assume A6: z in dom (r (#) (f * I)) ; :: thesis: (r (#) (f * I)) . z = ((r (#) f) * I) . z
then A7: z in dom (f * I) by VFUNCT_1:def 4;
A9: f /. (I . z) = f . (I . z) by A1, A5, A4a, A6, PARTFUN1:def 6
.= (f * I) . z by A7, FUNCT_1:12
.= (f * I) /. z by A7, PARTFUN1:def 6 ;
A10: (r (#) (f * I)) . z = (r (#) (f * I)) /. z by A6, PARTFUN1:def 6
.= r * (f /. (I . z)) by A6, A9, VFUNCT_1:def 4 ;
((r (#) f) * I) . z = (r (#) f) . (I . z) by A2, A4b, A6, FUNCT_1:12
.= (r (#) f) /. (I . z) by A5, A4a, A6, PARTFUN1:def 6
.= r * (f /. (I . z)) by A5, A4a, A6, VFUNCT_1:def 4 ;
hence (r (#) (f * I)) . z = ((r (#) f) * I) . z by A10; :: thesis: verum

end;

hence r (#) (f * I) = (r (#) f) * I by A4, TARSKI:2, PARTFUN1:5; :: thesis: verum