defpred S1[ 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: S1[ 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 ;
then reconsider m = <*1*> as non empty FinSequence of INT by FINSEQ_1:def 4;
A4: len m = (len b) + 1 by ;
A5: m . 1 = 1 by FINSEQ_1:40;
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 ; :: thesis: verum
end;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[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 ;
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 ;
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 ;
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
.= (len b) + 1 by ;
A16: rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) = (rng m1) \/ {((Product (b | k)) * (b . (len b)))} by ;
rng m1 c= INT by FINSEQ_1:def 4;
then rng (m1 ^ <*((Product (b | k)) * (b . (len b)))*>) c= INT by ;
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 ;
( 1 <= 1 & 1 <= k + 1 ) by NAT_1:12;
then 1 in dom m1 by ;
then A18: m . 1 = 1 by ;
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 ;
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 ;
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
.= (m . i) * (b . i) by ; :: thesis: verum
end;
suppose i <> len b ; :: thesis: m . (i + 1) = (m . i) * (b . i)
then A24: i < len b by ;
then A25: ( 1 <= i & i <= len (b | k) ) by ;
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 ;
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 ;
then A30: b . i = (b | k) . i by FUNCT_1:49;
A31: m . i = m1 . i by ;
thus m . (i + 1) = (m . i) * (b . i) by ; :: thesis: verum
end;
end;
end;
b | (k + 1) = (b | k) ^ <*(b . (len b))*> by ;
then A32: b = (b | k) ^ <*(b . (len b))*> by ;
len b in Seg (len m1) by ;
then A33: len b in dom m1 by FINSEQ_1:def 3;
A34: ( 1 <= len b & len b <= len b ) by ;
Product b = (m1 . ((len (b | k)) + 1)) * (b . (len b)) by
.= (m1 . (len b)) * (b . (len b)) by
.= (m . (len b)) * (b . (len b)) by
.= m . ((len b) + 1) by ;
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 ; :: thesis: verum
end;
for k being Nat holds S1[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