let i be Nat; for X being natural-valued positive-yielding XFinSequence st i in dom X holds
X . i <= Product X
defpred S1[ Nat] means for X being natural-valued positive-yielding XFinSequence
for i being Nat st len X = $1 & i in dom X holds
X . i <= Product X;
A1:
S1[ 0 ]
by XBOOLE_0:def 1;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
set n1 =
n + 1;
assume A3:
S1[
n]
;
S1[n + 1]
let X be
natural-valued positive-yielding XFinSequence;
for i being Nat st len X = n + 1 & i in dom X holds
X . i <= Product Xlet i be
Nat;
( len X = n + 1 & i in dom X implies X . i <= Product X )
assume A4:
(
len X = n + 1 &
i in dom X )
;
X . i <= Product X
then
X = (X | n) ^ <%(X . n)%>
by AFINSQ_1:56;
then A5:
Product X =
(Product (X | n)) * (Product <%(X . n)%>)
by Th7
.=
(Product (X | n)) * (X . n)
by Th5
;
A6:
n < n + 1
by NAT_1:13;
then A7:
(
n in dom X &
len (X | n) = n )
by A4, AFINSQ_1:54, AFINSQ_1:66;
then
(
Product (X | n) > 0 &
X . n in rng X )
by FUNCT_1:def 3;
then A8:
(
X . n > 0 &
Product (X | n) >= 1 )
by PARTFUN3:def 1, NAT_1:14;
then A9:
X . n >= 1
by NAT_1:14;
i < len X
by A4, AFINSQ_1:66;
then
i <= n
by A4, NAT_1:13;
per cases then
( i = n or i < n )
by XXREAL_0:1;
suppose A10:
i < n
;
X . i <= Product Xthen A11:
i in dom (X | n)
by A7, AFINSQ_1:66;
Product (X | n) >= (X | n) . i
by A3, A7, AFINSQ_1:66, A10;
then
(
Product X >= ((X | n) . i) * 1 &
(X | n) . i = X . i )
by A6, A4, AFINSQ_1:53, A11, A7, A5, A9, XREAL_1:66;
hence
X . i <= Product X
;
verum end; end;
end;
A12:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
let X be natural-valued positive-yielding XFinSequence; ( i in dom X implies X . i <= Product X )
thus
( i in dom X implies X . i <= Product X )
by A12; verum