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 & len (a * pf) = len pf )
by MATRIXR1:16;
then A3:
( dom (a * p) = Seg (len p) & Seg (len p) = dom p & dom (a * pf) = Seg (len pf) & Seg (len pf) = dom pf )
by FINSEQ_1:def 3;
then A4:
( dom ((a * p) * f) = dom f & dom (a * pf) = dom f )
by A1, A2, RELAT_1:46;
now let x be
set ;
:: thesis: ( x in dom (a * pf) implies (a * pf) . x = ((a * p) * f) . x )assume A5:
x in dom (a * pf)
;
:: thesis: (a * pf) . x = ((a * p) * f) . xset KK = the
carrier of
K;
f . x in rng f
by A4, A5, FUNCT_1:def 5;
then A6:
(
f . x in dom p &
p . (f . x) in rng p &
rng p c= the
carrier of
K &
pf . x in rng pf &
rng pf c= the
carrier of
K )
by A2, A3, A5, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider pf'x =
pf . x as
Element of
K ;
thus (a * pf) . x =
a * pf'x
by A5, FVSUM_1:62
.=
(a * p) . (f . x)
by A1, A3, A5, A6, FUNCT_1:22, FVSUM_1:62
.=
((a * p) * f) . x
by A4, A5, FUNCT_1:22
;
:: thesis: verum end;
hence
(a * p) * f = a * pf
by A4, FUNCT_1:9; :: thesis: verum