let S be RealNormSpace; :: thesis: for h being PartFunc of REAL, the carrier of S

for seq being Real_Sequence

for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

let h be PartFunc of REAL, the carrier of S; :: thesis: for seq being Real_Sequence

for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

let seq be Real_Sequence; :: thesis: for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

let r be Real; :: thesis: ( rng seq c= dom h implies (r (#) h) /* seq = r * (h /* seq) )

assume A1: rng seq c= dom h ; :: thesis: (r (#) h) /* seq = r * (h /* seq)

then A2: rng seq c= dom (r (#) h) by VFUNCT_1:def 4;

for seq being Real_Sequence

for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

let h be PartFunc of REAL, the carrier of S; :: thesis: for seq being Real_Sequence

for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

let seq be Real_Sequence; :: thesis: for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

let r be Real; :: thesis: ( rng seq c= dom h implies (r (#) h) /* seq = r * (h /* seq) )

assume A1: rng seq c= dom h ; :: thesis: (r (#) h) /* seq = r * (h /* seq)

then A2: rng seq c= dom (r (#) h) by VFUNCT_1:def 4;

now :: thesis: for n being Nat holds ((r (#) h) /* seq) . n = r * ((h /* seq) . n)

hence
(r (#) h) /* seq = r * (h /* seq)
by NORMSP_1:def 5; :: thesis: verumlet n be Nat; :: thesis: ((r (#) h) /* seq) . n = r * ((h /* seq) . n)

A3: n in NAT by ORDINAL1:def 12;

A4: seq . n in dom (r (#) h) by A2, Th1;

thus ((r (#) h) /* seq) . n = (r (#) h) /. (seq . n) by A2, FUNCT_2:109, A3

.= r * (h /. (seq . n)) by A4, VFUNCT_1:def 4

.= r * ((h /* seq) . n) by A1, FUNCT_2:109, A3 ; :: thesis: verum

end;A3: n in NAT by ORDINAL1:def 12;

A4: seq . n in dom (r (#) h) by A2, Th1;

thus ((r (#) h) /* seq) . n = (r (#) h) /. (seq . n) by A2, FUNCT_2:109, A3

.= r * (h /. (seq . n)) by A4, VFUNCT_1:def 4

.= r * ((h /* seq) . n) by A1, FUNCT_2:109, A3 ; :: thesis: verum