let G be Group; for F1, F2 being FinSequence of the carrier of G st len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) "
let F1, F2 be FinSequence of the carrier of G; ( len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
defpred S1[ Element of NAT ] means for F1, F2 being FinSequence of the carrier of G st len F1 = $1 & len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) holds
Product F1 = (Product F2) " ;
A1:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be
Element of
NAT ;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
let F1,
F2 be
FinSequence of the
carrier of
G;
( len F1 = n + 1 & len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
assume that A3:
len F1 = n + 1
and A4:
len F1 = len F2
and A5:
for
k being
Element of
NAT st
k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) "
;
Product F1 = (Product F2) "
reconsider p =
F1 | (Seg n) as
FinSequence of the
carrier of
G by FINSEQ_1:18;
deffunc H1(
Nat)
-> set =
F2 . ($1 + 1);
consider q being
FinSequence such that A6:
len q = len p
and A7:
for
k being
Nat st
k in dom q holds
q . k = H1(
k)
from FINSEQ_1:sch 2();
A8:
dom q = dom p
by A6, FINSEQ_3:29;
A9:
len p = n
by A3, FINSEQ_3:53;
A10:
rng q c= the
carrier of
G
A15:
rng F1 c= the
carrier of
G
by FINSEQ_1:def 4;
1
<= n + 1
by NAT_1:12;
then
n + 1
in dom F1
by A3, FINSEQ_3:25;
then
F1 . (n + 1) in rng F1
by FUNCT_1:def 3;
then reconsider a =
F1 . (n + 1) as
Element of
G by A15;
A16:
F1 = p ^ <*a*>
by A3, FINSEQ_3:55;
A17:
now let k be
Element of
NAT ;
( k in dom <*(a ")*> implies <*(a ")*> . k = F2 . k )assume
k in dom <*(a ")*>
;
<*(a ")*> . k = F2 . kthen A18:
k in {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
len F2 >= 1
by A3, A4, NAT_1:12;
then A19:
len F2 in dom F1
by A4, FINSEQ_3:25;
then
F2 . (((len F1) - (len F1)) + 1) = (F1 /. (len F1)) "
by A4, A5;
then
(F1 /. (len F1)) " = F2 . k
by A18, TARSKI:def 1;
then A20:
F2 . k = a "
by A3, A4, A19, PARTFUN1:def 6;
k = 1
by A18, TARSKI:def 1;
hence
<*(a ")*> . k = F2 . k
by A20, FINSEQ_1:def 8;
verum end;
reconsider q =
q as
FinSequence of the
carrier of
G by A10, FINSEQ_1:def 4;
now let k be
Element of
NAT ;
( k in dom p implies q . (((len p) - k) + 1) = (p /. k) " )assume A21:
k in dom p
;
q . (((len p) - k) + 1) = (p /. k) " then reconsider i =
((len p) - k) + 1 as
Element of
NAT by Lm3;
A22:
i + 1
= ((len F1) - k) + 1
by A3, A9;
( 1
<= i &
i <= len p )
by A21, Lm3;
then
i in dom p
by FINSEQ_3:25;
then A23:
q . i = F2 . (i + 1)
by A7, A8;
k <= len p
by A21, FINSEQ_3:25;
then A24:
k <= len F1
by A3, A9, NAT_1:12;
1
<= k
by A21, FINSEQ_3:25;
then A25:
k in dom F1
by A24, FINSEQ_3:25;
then F1 /. k =
F1 . k
by PARTFUN1:def 6
.=
p . k
by A21, FUNCT_1:47
.=
p /. k
by A21, PARTFUN1:def 6
;
hence
q . (((len p) - k) + 1) = (p /. k) "
by A5, A23, A25, A22;
verum end;
then A26:
Product p = (Product q) "
by A2, A9, A6;
len F2 = (len <*(a ")*>) + (len q)
by A3, A4, A9, A6, FINSEQ_1:39;
then
F2 = <*(a ")*> ^ q
by A17, A27, FINSEQ_3:38;
then Product F2 =
(a ") * (Product q)
by FINSOP_1:6
.=
(a ") * ((Product p) ")
by A26
.=
((Product p) * a) "
by GROUP_1:17
;
hence
Product F1 = (Product F2) "
by A16, FINSOP_1:4;
verum
end;
A29:
S1[ 0 ]
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A29, A1);
hence
( len F1 = len F2 & ( for k being Element of NAT st k in dom F1 holds
F2 . (((len F1) - k) + 1) = (F1 /. k) " ) implies Product F1 = (Product F2) " )
; verum