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 ((Product F),B) = Product G
let F be FinSequence of A; for G being FinSequence of B st A is Subring of B & F = G holds
In ((Product F),B) = Product G
let G be FinSequence of B; ( A is Subring of B & F = G implies In ((Product F),B) = Product G )
assume A0:
A is Subring of B
; ( not F = G or In ((Product F),B) = Product 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 ((Product F),B) = Product 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 ((Product F),B) = Product Glet G be
FinSequence of
B;
( len F = 0 & F = G implies In ((Product F),B) = Product G )
assume A1:
(
len F = 0 &
F = G )
;
In ((Product F),B) = Product G
then A2:
F = <*> the
carrier of
A
;
A3:
G = <*> the
carrier of
B
by A1;
In (
(Product F),
B) =
In (
(1_ A),
B)
by A2, GROUP_4:8
.=
In (
(1_ B),
B)
by A0, C0SP1:def 3
.=
Product G
by A3, GROUP_4:8
;
hence
In (
(Product F),
B)
= Product 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 ((Product F),B) = Product Glet G be
FinSequence of
B;
( len F = n + 1 & F = G implies In ((Product F),B) = Product G )
assume A5:
(
len F = n + 1 &
F = G )
;
In ((Product F),B) = Product 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
by FINSEQ_1:def 4;
then reconsider af =
F . (n + 1) as
Element of
A by A6, FUNCT_1:3;
B:
F = F0 ^ <*af*>
by A5, FINSEQ_3:55;
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
by FINSEQ_1:def 4;
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 Product G =
(Product G0) * bf
by GROUP_4:6
.=
(In ((Product F0),B)) * (In (af,B))
by A5, A4, A11
.=
In (
((Product F0) * af),
B)
by A0, ALGNUM_1:9
.=
In (
(Product F),
B)
by B, GROUP_4:6
;
hence
In (
(Product F),
B)
= Product G
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(P1, P2);
hence
( not F = G or In ((Product F),B) = Product G )
; verum