let F be non empty FinSequence of the carrier of (Polynom-Ring INT.Ring); Product (^ F) = ^ (Product F)
set L = INT.Ring ;
set PRI = Polynom-Ring INT.Ring;
for k being non zero Nat st len F = k holds
Product (^ F) = ^ (Product F)
proof
let k be non
zero Nat;
( len F = k implies Product (^ F) = ^ (Product F) )
defpred S1[
Nat]
means for
F being
FinSequence of the
carrier of
(Polynom-Ring INT.Ring) st
len F = $1 holds
Product (^ F) = ^ (Product F);
A1:
S1[1]
proof
for
F being
FinSequence of the
carrier of
(Polynom-Ring INT.Ring) st
len F = 1 holds
Product (^ F) = ^ (Product F)
proof
let F be
FinSequence of the
carrier of
(Polynom-Ring INT.Ring);
( len F = 1 implies Product (^ F) = ^ (Product F) )
assume A2:
len F = 1
;
Product (^ F) = ^ (Product F)
then
dom F = Seg 1
by FINSEQ_1:def 3;
then A3:
1
in dom F
;
then
F . 1
in rng F
by FUNCT_1:3;
then reconsider F1 =
F . 1 as
Element of
(Polynom-Ring INT.Ring) ;
A4:
Seg (len (^ F)) =
dom (^ F)
by FINSEQ_1:def 3
.=
dom F
by Def7
.=
Seg (len F)
by FINSEQ_1:def 3
;
A5:
F = <*F1*>
by A2, FINSEQ_1:40;
A6:
^ (Product F) = ^ F1
by A5, GROUP_4:9;
A7:
F /. 1
= F1
by A3, PARTFUN1:def 6;
A8:
(^ F) . 1
= ^ F1
by A7, A3, Def7;
reconsider RF1 =
^ F1 as
Element of
(Polynom-Ring F_Real) ;
reconsider RF =
^ F as
FinSequence of the
carrier of
(Polynom-Ring F_Real) ;
RF = <*(^ F1)*>
by A8, A2, A4, FINSEQ_1:6, FINSEQ_1:40;
hence
Product (^ F) = ^ (Product F)
by A6, GROUP_4:9;
verum
end;
hence
S1[1]
;
verum
end;
A10:
for
k being non
zero Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be non
zero Nat;
( S1[k] implies S1[k + 1] )
assume A11:
S1[
k]
;
S1[k + 1]
for
F being
FinSequence of the
carrier of
(Polynom-Ring INT.Ring) st
len F = k + 1 holds
Product (^ F) = ^ (Product F)
proof
let F be
FinSequence of the
carrier of
(Polynom-Ring INT.Ring);
( len F = k + 1 implies Product (^ F) = ^ (Product F) )
assume A12:
len F = k + 1
;
Product (^ F) = ^ (Product F)
then consider G being
FinSequence of
(Polynom-Ring INT.Ring),
d being
Element of
(Polynom-Ring INT.Ring) such that A13:
F = G ^ <*d*>
by FINSEQ_2:19;
A14:
Seg (len F) =
dom F
by FINSEQ_1:def 3
.=
dom (^ F)
by Def7
.=
Seg (len (^ F))
by FINSEQ_1:def 3
;
dom F = Seg (k + 1)
by A12, FINSEQ_1:def 3;
then A15:
dom (^ F) = Seg (k + 1)
by Def7;
(F | k) ^ <*(F /. (len F))*> = G ^ <*d*>
by A13, A12, FINSEQ_5:21;
then A16:
(
G = F | k &
d = F /. (len F) )
by FINSEQ_2:17;
A17:
k + 1
= (len G) + 1
by FINSEQ_2:16, A13, A12;
reconsider RF =
^ F as
FinSequence of the
carrier of
(Polynom-Ring F_Real) ;
len F in Seg (len F)
by A12, FINSEQ_1:3;
then A18:
len F in dom F
by FINSEQ_1:def 3;
reconsider Fl =
F /. (len F) as
Element of the
carrier of
(Polynom-Ring INT.Ring) ;
A19:
len RF = len F
by A14, FINSEQ_1:6;
len RF in dom F
by A14, FINSEQ_1:6, A18;
then
len RF in dom RF
by Def7;
then A20:
RF /. (len RF) =
RF . (len RF)
by PARTFUN1:def 6
.=
(^ F) . (len F)
by A14, FINSEQ_1:6
.=
^ Fl
by A18, Def7
;
Product F = (Product G) * d
by A13, GROUP_4:6;
then ^ (Product F) =
(^ (Product G)) * (^ d)
by Th27
.=
(Product (^ (F | k))) * (^ (F /. (len F)))
by A17, A11, A16
.=
(Product ((^ F) | k)) * (^ Fl)
by A12, Lm16
.=
Product (((^ F) | k) ^ <*(^ Fl)*>)
by GROUP_4:6
.=
Product (RF | (k + 1))
by A19, A12, FINSEQ_5:82, A20
.=
Product (^ F)
by A15
;
hence
Product (^ F) = ^ (Product F)
;
verum
end;
hence
S1[
k + 1]
;
verum
end;
for
k being non
zero Nat holds
S1[
k]
from NAT_1:sch 10(A1, A10);
hence
(
len F = k implies
Product (^ F) = ^ (Product F) )
;
verum
end;
hence
Product (^ F) = ^ (Product F)
; verum