let X, Y, W be RealNormSpace; 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; 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; for r being Real holds r (#) (f * I) = (r (#) f) * I
let r be Real; 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) )
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) )
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;
( z in dom (r (#) (f * I)) implies (r (#) (f * I)) . z = ((r (#) f) * I) . z )
assume A6:
z in dom (r (#) (f * I))
;
(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;
verum
end;
hence
r (#) (f * I) = (r (#) f) * I
by A4, TARSKI:2, PARTFUN1:5; verum