let K be Field; :: thesis: for a being Element of K
for p, pf being FinSequence of K
for f being Function st pf = p * f & rng f c= dom p holds
(a * p) * f = a * pf
let a be Element of K; :: thesis: for p, pf being FinSequence of K
for f being Function st pf = p * f & rng f c= dom p holds
(a * p) * f = a * pf
let p, pf be FinSequence of K; :: thesis: for f being Function st pf = p * f & rng f c= dom p holds
(a * p) * f = a * pf
let f be Function; :: thesis: ( pf = p * f & rng f c= dom p implies (a * p) * f = a * pf )
assume that
A1: pf = p * f and
A2: rng f c= dom p ; :: thesis: (a * p) * f = a * pf
len (a * p) = len p by MATRIXR1:16;
then A3: dom (a * p) = Seg (len p) by FINSEQ_1:def 3;
A4: Seg (len p) = dom p by FINSEQ_1:def 3;
then A5: dom ((a * p) * f) = dom f by A2, A3, RELAT_1:27;
len (a * pf) = len pf by MATRIXR1:16;
then A6: dom (a * pf) = Seg (len pf) by FINSEQ_1:def 3;
A7: Seg (len pf) = dom pf by FINSEQ_1:def 3;
then A8: dom (a * pf) = dom f by A1, A2, A6, RELAT_1:27;

now :: thesis: for x being object st x in dom (a * pf) holds
(a * pf) . x = ((a * p) * f) . x

set KK = the carrier of K;
A9: rng pf c= the carrier of K by FINSEQ_1:def 4;
let x be object ; :: thesis: ( x in dom (a * pf) implies (a * pf) . x = ((a * p) * f) . x )
assume A10: x in dom (a * pf) ; :: thesis: (a * pf) . x = ((a * p) * f) . x
A11: f . x in rng f by A8, A10, FUNCT_1:def 3;
then A12: f . x in dom p by A2;
pf . x in rng pf by A6, A7, A10, FUNCT_1:def 3;
then reconsider pf9x = pf . x as Element of K by A9;
A13: p . (f . x) in rng p by A2, A11, FUNCT_1:def 3;
thus (a * pf) . x = a * pf9x by A10, FVSUM_1:50
.= (a * p) . (f . x) by A1, A3, A4, A6, A7, A10, A12, A13, FUNCT_1:12, FVSUM_1:50
.= ((a * p) * f) . x by A5, A8, A10, FUNCT_1:12 ; :: thesis: verum

end;

hence (a * p) * f = a * pf by A1, A2, A6, A7, A5, FUNCT_1:2, RELAT_1:27; :: thesis: verum