let R be Ring; for S being Subring of R
for f being FinSequence of R
for g being FinSequence of S st f = g holds
Sum f = Sum g
let S be Subring of R; for f being FinSequence of R
for g being FinSequence of S st f = g holds
Sum f = Sum g
let f be FinSequence of R; for g being FinSequence of S st f = g holds
Sum f = Sum g
let g be FinSequence of S; ( f = g implies Sum f = Sum g )
assume AS:
f = g
; Sum f = Sum g
defpred S1[ Nat] means for f being FinSequence of R
for g being FinSequence of S st f = g & len f = $1 holds
Sum f = Sum g;
then A:
S1[ 0 ]
;
AS4:
the carrier of S c= the carrier of R
by C0SP1:def 3;
B:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume IA:
S1[
k]
;
S1[k + 1]now for f being FinSequence of R
for g being FinSequence of S st f = g & len f = k + 1 holds
Sum f = Sum glet f be
FinSequence of
R;
for g being FinSequence of S st f = g & len f = k + 1 holds
Sum f = Sum glet g be
FinSequence of
S;
( f = g & len f = k + 1 implies Sum f = Sum g )assume B0:
(
f = g &
len f = k + 1 )
;
Sum f = Sum gthen
g <> {}
;
then consider h being
FinSequence,
x being
object such that B1:
g = h ^ <*x*>
by FINSEQ_1:46;
reconsider h =
h,
o =
<*x*> as
FinSequence of
S by B1, FINSEQ_1:36;
len o = 1
by FINSEQ_1:39;
then B2:
len g = (len h) + 1
by B1, FINSEQ_1:22;
C2:
dom g = Seg (k + 1)
by B0, FINSEQ_1:def 3;
B4:
1
<= k + 1
by NAT_1:11;
x = g . (k + 1)
by B0, B2, B1, FINSEQ_1:42;
then reconsider x =
x as
Element of
S by B4, C2, FINSEQ_1:1, FINSEQ_2:11;
reconsider y =
x as
Element of
R by AS4;
rng h c= the
carrier of
R
by AS4;
then reconsider hh =
h as
FinSequence of
R by FINSEQ_1:def 4;
rng o c= the
carrier of
R
by AS4;
then reconsider oo =
o as
FinSequence of
R by FINSEQ_1:def 4;
dom the
addF of
S = [: the carrier of S, the carrier of S:]
by FUNCT_2:def 1;
then B7:
[(Sum h),(Sum o)] in dom the
addF of
S
;
B8:
Sum o =
y
by RLVECT_1:44
.=
Sum oo
by RLVECT_1:44
;
thus Sum f =
(Sum hh) + (Sum oo)
by B0, B1, RLVECT_1:41
.=
the
addF of
R . (
(Sum h),
(Sum o))
by B8, B0, B2, IA
.=
( the addF of R || the carrier of S) . (
(Sum h),
(Sum o))
by B7, FUNCT_1:49
.=
(Sum h) + (Sum o)
by C0SP1:def 3
.=
Sum g
by B1, RLVECT_1:41
;
verum end; hence
S1[
k + 1]
;
verum end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 2(A, B);
consider n being Nat such that
H:
len f = n
;
thus
Sum f = Sum g
by AS, I, H; verum