let K be Ring; for p, q being FinSequence of K
for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
( Sum (mlt (p,q)) = q . i & Sum (mlt (q,p)) = q . i )
let p, q be FinSequence of K; for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
( Sum (mlt (p,q)) = q . i & Sum (mlt (q,p)) = q . i )
let i be Nat; ( i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) implies ( Sum (mlt (p,q)) = q . i & Sum (mlt (q,p)) = q . i ) )
assume that
A1:
( i in dom p & i in dom q )
and
A2:
( p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) )
; ( Sum (mlt (p,q)) = q . i & Sum (mlt (q,p)) = q . i )
thus
Sum (mlt (p,q)) = q . i
Sum (mlt (q,p)) = q . iproof
reconsider r =
mlt (
p,
q) as
FinSequence of
K ;
A3:
for
k being
Nat st
k in dom r &
k <> i holds
r . k = 0. K
by A2, Th14;
A4:
(
dom p = Seg (len p) &
dom q = Seg (len q) )
by FINSEQ_1:def 3;
(
dom (mlt (p,q)) = Seg (len (mlt (p,q))) &
len (mlt (p,q)) = min (
(len p),
(len q)) )
by Th13, FINSEQ_1:def 3;
then
(dom p) /\ (dom q) = dom (mlt (p,q))
by A4, FINSEQ_2:2;
then A5:
i in dom r
by A1, XBOOLE_0:def 4;
then
r . i = q . i
by A2, Th14;
hence
Sum (mlt (p,q)) = q . i
by A5, A3, Th12;
verum
end;
thus
Sum (mlt (q,p)) = q . i
verumproof
reconsider r =
mlt (
q,
p) as
FinSequence of
K ;
A6:
for
k being
Nat st
k in dom r &
k <> i holds
r . k = 0. K
by A2, Th14;
A7:
(
dom p = Seg (len p) &
dom q = Seg (len q) )
by FINSEQ_1:def 3;
(
dom (mlt (q,p)) = Seg (len (mlt (q,p))) &
len (mlt (q,p)) = min (
(len q),
(len p)) )
by Th13, FINSEQ_1:def 3;
then
(dom q) /\ (dom p) = dom (mlt (q,p))
by A7, FINSEQ_2:2;
then A8:
i in dom r
by A1, XBOOLE_0:def 4;
then
r . i = q . i
by A2, Th14;
hence
Sum (mlt (q,p)) = q . i
by A8, A6, Th12;
verum
end;