let A, B be Ring; for F being FinSequence of A
for G being FinSequence of B st A is Subring of B & F = G holds
In ((Sum F),B) = Sum G
let F be FinSequence of A; for G being FinSequence of B st A is Subring of B & F = G holds
In ((Sum F),B) = Sum G
let G be FinSequence of B; ( A is Subring of B & F = G implies In ((Sum F),B) = Sum G )
assume A0:
A is Subring of B
; ( not F = G or In ((Sum F),B) = Sum G )
defpred S1[ Nat] means for F being FinSequence of A
for G being FinSequence of B st len F = $1 & F = G holds
In ((Sum F),B) = Sum G;
P1:
S1[ 0 ]
proof
let F be
FinSequence of
A;
for G being FinSequence of B st len F = 0 & F = G holds
In ((Sum F),B) = Sum Glet G be
FinSequence of
B;
( len F = 0 & F = G implies In ((Sum F),B) = Sum G )
assume A1:
(
len F = 0 &
F = G )
;
In ((Sum F),B) = Sum G
then A2:
F = <*> the
carrier of
A
;
A3:
G = <*> the
carrier of
B
by A1;
In (
(Sum F),
B) =
In (
(0. A),
B)
by A2, RLVECT_1:43
.=
In (
(0. B),
B)
by A0, C0SP1:def 3
.=
0. B
by SUBSET_1:def 8
.=
Sum G
by A3, RLVECT_1:43
;
hence
In (
(Sum F),
B)
= Sum G
;
verum
end;
P2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
let F be
FinSequence of
A;
for G being FinSequence of B st len F = n + 1 & F = G holds
In ((Sum F),B) = Sum Glet G be
FinSequence of
B;
( len F = n + 1 & F = G implies In ((Sum F),B) = Sum G )
assume A5:
(
len F = n + 1 &
F = G )
;
In ((Sum F),B) = Sum G
reconsider F0 =
F | n as
FinSequence of
A ;
n + 1
in Seg (n + 1)
by FINSEQ_1:4;
then A6:
n + 1
in dom F
by A5, FINSEQ_1:def 3;
rng F c= the
carrier of
A
;
then reconsider af =
F . (n + 1) as
Element of
A by A6, FUNCT_1:3;
A7:
len F0 = n
by FINSEQ_1:59, A5, NAT_1:11;
A8:
len F = (len F0) + 1
by A5, FINSEQ_1:59, NAT_1:11;
A9:
F0 = F | (dom F0)
by A7, FINSEQ_1:def 3;
reconsider G0 =
G | n as
FinSequence of
B ;
n + 1
in Seg (n + 1)
by FINSEQ_1:4;
then A10:
n + 1
in dom G
by A5, FINSEQ_1:def 3;
rng G c= the
carrier of
B
;
then reconsider bf =
G . (n + 1) as
Element of
B by A10, FUNCT_1:3;
A11:
(
len F0 = n &
F0 = G0 )
by FINSEQ_1:59, A5, NAT_1:11;
G = G0 ^ <*bf*>
by A5, FINSEQ_3:55;
then Sum G =
(Sum G0) + bf
by FVSUM_1:71
.=
(In ((Sum F0),B)) + bf
by A4, A11
.=
(In ((Sum F0),B)) + (In (af,B))
by A5, SUBSET_1:def 8
.=
In (
((Sum F0) + af),
B)
by A0, Th12
.=
In (
(Sum F),
B)
by A5, A8, A9, RLVECT_1:38
;
hence
In (
(Sum F),
B)
= Sum G
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(P1, P2);
hence
( not F = G or In ((Sum F),B) = Sum G )
; verum