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) );
A1: 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 A2: 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) )
A3: 1 in INT by INT_1:def 2;
rng <*1*> = {1} by FINSEQ_1:39;
then rng <*1*> c= INT by A3, ZFMISC_1:31;
then reconsider m = <*1*> as non empty FinSequence of INT by FINSEQ_1:def 4;
A4: len m = (len b) + 1 by A2, FINSEQ_1:40;
A5: m . 1 = 1 ;
A6: for i being Nat st 1 <= i & i <= len b holds
m . (i + 1) = (m . i) * (b . i) by A2;
b = <*> REAL by A2;
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 A4, A5, A6, RVSUM_1:94; :: thesis: verum

end;

A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: 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 A9: 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;
A10: len (b | k) = k by A9, FINSEQ_1:59, NAT_1:12;
then consider m1 being non empty FinSequence of INT such that
A11: ( (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 A8;
set m = m1 ^ <*((Product (b | k)) * (b . (len b)))*>;
A12: (Product (b | k)) * (b . (len b)) in INT by A11, INT_1:def 2;
A13: rng <*((Product (b | k)) * (b . (len b)))*> = {((Product (b | k)) * (b . (len b)))} by FINSEQ_1:39;
then A14: rng <*((Product (b | k)) * (b . (len b)))*> c= INT by A12, ZFMISC_1:31;
A15: 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 A11, FINSEQ_1:40
.= (len b) + 1 by A9, FINSEQ_1:59, NAT_1:12 ;
A16: rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (rng m1) \/ {((Product (b | k)) * (b . (len b)))} by A13, FINSEQ_1:31;
rng m1 c= INT by FINSEQ_1:def 4;
then rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) c= INT by A13, A16, A14, XBOOLE_1:8;
then reconsider m = m1 ^ <*((Product (b | k)) * (b . (len b)))*> as non empty FinSequence of INT by FINSEQ_1:def 4;
A17: len m1 = k + 1 by A9, FINSEQ_1:59, NAT_1:12, A11;
( 1 <= 1 & 1 <= k + 1 ) by NAT_1:12;
then 1 in dom m1 by A17, FINSEQ_3:25;
then A18: m . 1 = 1 by A11, FINSEQ_1:def 7;
A19: 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 A20: ( 1 <= i & i <= len b ) ; :: thesis: m . (i + 1) = (m . i) * (b . i)

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

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

(len (b | k)) + 1 in Seg (len m1) by A10, A17, FINSEQ_1:4;
then (len (b | k)) + 1 in dom m1 by FINSEQ_1:def 3;
then A22: m1 . ((len (b | k)) + 1) = m . ((len (b | k)) + 1) by FINSEQ_1:def 7
.= m . i by A9, A21, FINSEQ_1:59, NAT_1:12 ;
1 in Seg 1 ;
then A23: 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 A21, A9, A17, A23, FINSEQ_1:def 7
.= (m . i) * (b . i) by A22, A21, A11 ; :: thesis: verum

end;

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

then A24: i < len b by A20, XXREAL_0:1;
then A25: ( 1 <= i & i <= len (b | k) ) by A10, A9, A20, NAT_1:13;
then A26: m1 . (i + 1) = (m1 . i) * ((b | k) . i) by A11;
i in Seg (len m1) by A20, A9, A17;
then A27: i in dom m1 by FINSEQ_1:def 3;
A28: i + 1 <= len m1 by A9, A17, A24, NAT_1:13;
1 <= i + 1 by NAT_1:12;
then i + 1 in Seg (len m1) by A28;
then A29: i + 1 in dom m1 by FINSEQ_1:def 3;
i in Seg k by A25, A10;
then A30: b . i = (b | k) . i by FUNCT_1:49;
A31: m . i = m1 . i by A27, FINSEQ_1:def 7;
thus m . (i + 1) = (m . i) * (b . i) by A26, A29, A30, A31, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

b | (k + 1) = (b | k) ^ <*(b . (len b))*> by A9, INT_6:5;
then A32: b = (b | k) ^ <*(b . (len b))*> by A9, FINSEQ_1:58;
len b in Seg (len m1) by A9, A17, FINSEQ_1:4;
then A33: len b in dom m1 by FINSEQ_1:def 3;
A34: ( 1 <= len b & len b <= len b ) by A9, NAT_1:12;
Product b = (m1 . ((len (b | k)) + 1)) * (b . (len b)) by A11, A32, RVSUM_1:96
.= (m1 . (len b)) * (b . (len b)) by A9, FINSEQ_1:59, NAT_1:12
.= (m . (len b)) * (b . (len b)) by A33, FINSEQ_1:def 7
.= m . ((len b) + 1) by A19, A34 ;
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 A15, A18, A19; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A7);
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