defpred S₁[ Nat] means for b being FinSequence of INT st len b = $1 holds
ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) );
P0: S₁[ 0 ]

proof

let b be FinSequence of INT ; :: thesis: ( len b = 0 implies ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) )
assume A1: len b = 0 ; :: thesis: ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )
I0: 1 in INT by INT_1:def 2;
rng <*1*> = {1} by FINSEQ_1:39;
then rng <*1*> c= INT by ZFMISC_1:31, I0;
then reconsider m = <*1*> as non empty FinSequence of INT by FINSEQ_1:def 4;
P0: len m = (len b) + 1 by A1, FINSEQ_1:40;
P1: m . 1 = 1 by FINSEQ_1:40;
P2: for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) by A1;
b = <*> REAL by A1;
hence ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by P0, P1, P2, A1, RVSUM_1:94; :: thesis: verum

end;

P1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A1: S₁[k] ; :: thesis: S₁[k + 1]
let b be FinSequence of INT ; :: thesis: ( len b = k + 1 implies ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) )
assume A2: len b = k + 1 ; :: thesis: ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) )
set b1 = b | k;
P2: len (b | k) = k by FINSEQ_1:59, A2, NAT_1:12;
then consider m1 being non empty FinSequence of INT such that
P4: ( (len (b | k)) + 1 = len m1 & m1 . 1 = 1 & ( for i being Nat st 1 <= i & i <= len (b | k) holds
m1 . (i + 1) = (m1 . i) * ((b | k) . i) ) & Product (b | k) = m1 . ((len (b | k)) + 1) ) by A1;
set m = m1 ^ <*((Product (b | k)) * (b . (len b)))*>;
P5Z: (Product (b | k)) * (b . (len b)) in INT by P4, INT_1:def 2;
P5W: rng <*((Product (b | k)) * (b . (len b)))*> = {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:39;
then P5Q: rng <*((Product (b | k)) * (b . (len b)))*> c= INT by ZFMISC_1:31, P5Z;
P5: len (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (len m1) + (len <*((Product (b | k)) * (b . (len b)))*>) by FINSEQ_1:22
.= ((len (b | k)) + 1) + 1 by P4, FINSEQ_1:40
.= (len b) + 1 by FINSEQ_1:59, A2, NAT_1:12 ;
VV2: rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (rng m1) \/ {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:31, P5W;
rng m1 c= INT by FINSEQ_1:def 4;
then rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) c= INT by P5W, VV2, P5Q, XBOOLE_1:8;
then reconsider m = m1 ^ <*((Product (b | k)) * (b . (len b)))*> as non empty FinSequence of INT by FINSEQ_1:def 4;
P5B: len m1 = (len (b | k)) + 1 by P4
.= k + 1 by FINSEQ_1:59, A2, NAT_1:12 ;
( 1 <= 1 & 1 <= k + 1 ) by NAT_1:12;
then 1 in Seg (len m1) by P5B;
then 1 in dom m1 by FINSEQ_1:def 3;
then P8: m . 1 = 1 by P4, FINSEQ_1:def 7;
P9: for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i)

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len b implies m . (i + 1) = (m . i) * (b . i) )
assume P10: ( 1 <= i & i <= len b ) ; :: thesis: m . (i + 1) = (m . i) * (b . i)

per cases ( i = len b or i <> len b ) ;

suppose P11: i = len b ; :: thesis: m . (i + 1) = (m . i) * (b . i)

(len (b | k)) + 1 in Seg (len m1) by P2, P5B, FINSEQ_1:4;
then (len (b | k)) + 1 in dom m1 by FINSEQ_1:def 3;
then P13: m1 . ((len (b | k)) + 1) = m . ((len (b | k)) + 1) by FINSEQ_1:def 7
.= m . i by A2, FINSEQ_1:59, NAT_1:12, P11 ;
1 in Seg 1 ;
then P13C: 1 in dom <*((Product (b | k)) * (b . (len b)))*> by FINSEQ_1:38;
thus m . (i + 1) = <*((Product (b | k)) * (b . (len b)))*> . 1 by FINSEQ_1:def 7, P11, A2, P5B, P13C
.= (m . i) * (b . i) by P13, P11, P4, FINSEQ_1:40 ; :: thesis: verum

end;

suppose i <> len b ; :: thesis: m . (i + 1) = (m . i) * (b . i)

then P12D: i < len b by P10, XXREAL_0:1;
then P12A: ( 1 <= i & i <= len (b | k) ) by P2, A2, NAT_1:13, P10;
then P13: m1 . (i + 1) = (m1 . i) * ((b | k) . i) by P4;
i in Seg (len m1) by FINSEQ_1:1, P10, A2, P5B;
then P13B: i in dom m1 by FINSEQ_1:def 3;
P13E: i + 1 <= len m1 by A2, P5B, P12D, NAT_1:13;
1 <= i + 1 by NAT_1:12;
then i + 1 in Seg (len m1) by P13E;
then P13C: i + 1 in dom m1 by FINSEQ_1:def 3;
i in Seg k by P12A, FINSEQ_1:1, P2;
then P15: b . i = (b | k) . i by FUNCT_1:49;
P16: m . i = m1 . i by FINSEQ_1:def 7, P13B;
thus m . (i + 1) = (m . i) * (b . i) by P13, FINSEQ_1:def 7, P13C, P15, P16; :: thesis: verum

end;

end;

end;

b | (k + 1) = (b | k) ^ <*(b . (len b))*> by INT_6:5, A2;
then P17: b = (b | k) ^ <*(b . (len b))*> by FINSEQ_1:58, A2;
len b in Seg (len m1) by FINSEQ_1:4, A2, P5B;
then P18: len b in dom m1 by FINSEQ_1:def 3;
P19: ( 1 <= len b & len b <= len b ) by A2, NAT_1:12;
Product b = (m1 . ((len (b | k)) + 1)) * (b . (len b)) by P4, RVSUM_1:96, P17
.= (m1 . (len b)) * (b . (len b)) by A2, FINSEQ_1:59, NAT_1:12
.= (m . (len b)) * (b . (len b)) by FINSEQ_1:def 7, P18
.= m . ((len b) + 1) by P9, P19 ;
hence ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) by P5, P8, P9; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(P0, P1);
hence for b being FinSequence of INT ex m being non empty FinSequence of INT st
( len m = (len b) + 1 & m . 1 = 1 & ( for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) ) & Product b = m . ((len b) + 1) ) ; :: thesis: verum