let f1, f2 be FinSequence of REAL ; ( len f1 = len f2 & ( for i being Element of NAT st i in dom f1 holds
f2 . i = (f1 . i) " ) implies Product f2 = (Product f1) " )
defpred S1[ Nat] means for f1, f2 being FinSequence of REAL st len f1 = len f2 & $1 = len f1 & ( for k being Element of NAT st k in dom f1 holds
f2 . k = (f1 . k) " ) holds
Product f2 = (Product f1) " ;
assume A1:
len f1 = len f2
; ( ex i being Element of NAT st
( i in dom f1 & not f2 . i = (f1 . i) " ) or Product f2 = (Product f1) " )
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
for
f1,
f2 being
FinSequence of
REAL st
len f1 = len f2 &
n + 1
= len f1 & ( for
k being
Element of
NAT st
k in dom f1 holds
f2 . k = (f1 . k) " ) holds
Product f2 = (Product f1) "
proof
let f1,
f2 be
FinSequence of
REAL ;
( len f1 = len f2 & n + 1 = len f1 & ( for k being Element of NAT st k in dom f1 holds
f2 . k = (f1 . k) " ) implies Product f2 = (Product f1) " )
assume that A4:
len f1 = len f2
and A5:
n + 1
= len f1
;
( ex k being Element of NAT st
( k in dom f1 & not f2 . k = (f1 . k) " ) or Product f2 = (Product f1) " )
consider g2 being
FinSequence of
REAL ,
r2 being
Element of
REAL such that A6:
f2 = g2 ^ <*r2*>
by A4, A5, FINSEQ_2:19;
len f2 = (len g2) + (len <*r2*>)
by A6, FINSEQ_1:22;
then A7:
n + 1
= (len g2) + 1
by A4, A5, FINSEQ_1:39;
A8:
Product f2 = (Product g2) * r2
by A6, RVSUM_1:96;
consider g1 being
FinSequence of
REAL ,
r1 being
Element of
REAL such that A9:
f1 = g1 ^ <*r1*>
by A5, FINSEQ_2:19;
set k1 =
(len g1) + 1;
A10:
Product f1 = (Product g1) * r1
by A9, RVSUM_1:96;
len f1 = (len g1) + (len <*r1*>)
by A9, FINSEQ_1:22;
then A11:
n + 1
= (len g1) + 1
by A5, FINSEQ_1:39;
assume A12:
for
k being
Element of
NAT st
k in dom f1 holds
f2 . k = (f1 . k) "
;
Product f2 = (Product f1) "
A17:
Product g2 = (Product g1) "
by A3, A7, A11, A13;
n + 1
>= 0 + 1
by XREAL_1:6;
then
(len g1) + 1
in Seg (n + 1)
by A11;
then
(len g1) + 1
in dom f1
by A5, FINSEQ_1:def 3;
then A19:
f2 . ((len g1) + 1) = (f1 . ((len g1) + 1)) "
by A12;
(
r1 = f1 . ((len g1) + 1) &
r2 = f2 . ((len g1) + 1) )
by A6, A7, A9, A11, FINSEQ_1:42;
hence
Product f2 = (Product f1) "
by A8, A10, A17, A19, XCMPLX_1:204;
verum
end;
hence
S1[
n + 1]
;
verum
end;
A21:
S1[ 0 ]
A25:
for n being Nat holds S1[n]
from NAT_1:sch 2(A21, A2);
assume
for k being Element of NAT st k in dom f1 holds
f2 . k = (f1 . k) "
; Product f2 = (Product f1) "
hence
Product f2 = (Product f1) "
by A1, A25; verum