let f1, f2 be FinSequence of REAL ; :: thesis: ( 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 S₁[ 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 ; :: thesis: ( 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 S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[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 ; :: thesis: ( 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 ; :: thesis: ( 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) " ; :: thesis: Product f2 = (Product f1) "

A13: now :: thesis: for k being Element of NAT st k in dom g1 holds
g2 . k = (g1 . k) "

let k be Element of NAT ; :: thesis: ( k in dom g1 implies g2 . k = (g1 . k) " )
A14: dom g1 c= dom f1 by A9, FINSEQ_1:26;
assume A15: k in dom g1 ; :: thesis: g2 . k = (g1 . k) "
then k in Seg (len g2) by A7, A11, FINSEQ_1:def 3;
then k in dom g2 by FINSEQ_1:def 3;
then A16: f2 . k = g2 . k by A6, FINSEQ_1:def 7;
f1 . k = g1 . k by A9, A15, FINSEQ_1:def 7;
hence g2 . k = (g1 . k) " by A12, A14, A15, A16; :: thesis: verum

end;

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; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A21: S₁[ 0 ]

proof

let f1, f2 be FinSequence of REAL ; :: thesis: ( len f1 = len f2 & 0 = len f1 & ( for k being Element of NAT st k in dom f1 holds
f2 . k = (f1 . k) " ) implies Product f2 = (Product f1) " )
assume ( len f1 = len f2 & 0 = len f1 & ( for k being Element of NAT st k in dom f1 holds
f2 . k = (f1 . k) " ) ) ; :: thesis: Product f2 = (Product f1) "
then ( f1 = {} & f2 = {} ) ;
hence Product f2 = (Product f1) " by RVSUM_1:94; :: thesis: verum

end;

A25: for n being Nat holds S₁[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) " ; :: thesis: Product f2 = (Product f1) "
hence Product f2 = (Product f1) " by A1, A25; :: thesis: verum