let K be Field; 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; 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; for f being Function st pf = p * f & rng f c= dom p holds
(a * p) * f = a * pf
let f be Function; ( 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
; (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 for x being object st x in dom (a * pf) holds
(a * pf) . x = ((a * p) * f) . xset KK = the
carrier of
K;
A9:
rng pf c= the
carrier of
K
by FINSEQ_1:def 4;
let x be
object ;
( x in dom (a * pf) implies (a * pf) . x = ((a * p) * f) . x )assume A10:
x in dom (a * pf)
;
(a * pf) . x = ((a * p) * f) . xA11:
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
;
verum end;
hence
(a * p) * f = a * pf
by A1, A2, A6, A7, A5, FUNCT_1:2, RELAT_1:27; verum