let n be Nat; :: thesis: for f being natural-valued FinSequence st f <= n & f is increasing & f is positive-yielding holds
Product f divides n !
let f be natural-valued FinSequence; :: thesis: ( f <= n & f is increasing & f is positive-yielding implies Product f divides n ! )
set x = f . (len f);
assume that
A1: f <= n and
A2: f is increasing and
A3: f is positive-yielding ; :: thesis: Product f divides n !

per cases ( len f = 0 or len f > 0 ) ;

suppose len f = 0 ; :: thesis: Product f divides n !

then f = {} ;
hence Product f divides n ! by INT_2:12, RVSUM_1:94; :: thesis: verum

end;

suppose A4: len f > 0 ; :: thesis: Product f divides n !

defpred S₁[ Nat] means for f being natural-valued FinSequence st 0 < len f & len f = $1 & f <= n & f is increasing & f is positive-yielding holds
Product f divides (f . (len f)) ! ;
A5: S₁[ 0 ] ;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
let f be natural-valued FinSequence; :: thesis: ( 0 < len f & len f = k + 1 & f <= n & f is increasing & f is positive-yielding implies Product f divides (f . (len f)) ! )
assume that
A8: 0 < len f and
A9: len f = k + 1 and
A10: f <= n and
A11: f is increasing and
A12: f is positive-yielding ; :: thesis: Product f divides (f . (len f)) !
f <> {} by A8;
then consider g being FinSequence, x being object such that
A13: f = g ^ <*x*> by FINSEQ_1:46;
g is NAT -valued by A13, Th3;
then reconsider g = g as natural-valued FinSequence ;
len (g ^ <*x*>) = (len g) + (len <*x*>) by FINSEQ_1:22;
then A14: len f = (len g) + 1 by A13, FINSEQ_1:39;
then A15: x = f . (len f) by A13, FINSEQ_1:42;
then reconsider x = x as Nat ;
set y = g . (len g);
0 + 1 <= len f by A8, NAT_1:13;
then A16: len f in dom f by FINSEQ_3:25;
then A17: x in rng f by A15, FUNCT_1:def 3;

per cases ( len g = 0 or 0 < len g ) ;

suppose len g = 0 ; :: thesis: Product f divides (f . (len f)) !

then f = <*x*> by A13, FILEREC1:3;
hence Product f divides (f . (len f)) ! by A12, A15, NEWTON:35; :: thesis: verum

end;

suppose A18: 0 < len g ; :: thesis: Product f divides (f . (len f)) !

A19: (len f) - 1 < (len f) - 0 by XREAL_1:8;
A20: 0 + 1 <= len g by A18, NAT_1:13;
then A21: len g in dom f by A14, A19, FINSEQ_3:25;
A22: g <= n

proof

let q be object ; :: according to NUMBER08:def 4 :: thesis: ( q in dom g implies g . q <= n )
assume A23: q in dom g ; :: thesis: g . q <= n
A24: dom g c= dom f by A13, FINSEQ_1:26;
f . q = g . q by A13, A23, FINSEQ_1:def 7;
hence g . q <= n by A10, A23, A24; :: thesis: verum

end;

A25: <*x*> is ext-real-valued ;
then A26: g is increasing by A11, A13, Th36;
g is positive-yielding by A12, A13, A25, Th37;
then A27: Product g divides (g . (len g)) ! by A7, A9, A14, A18, A22, A26;
A28: (Product g) * x divides ((g . (len g)) !) * x by A27, NAT_3:1;
0 + 1 <= x by A12, A17, NAT_1:13;
then reconsider x1 = x - 1 as Element of NAT by INT_1:5;
len g in dom g by A20, FINSEQ_3:25;
then g . (len g) = f . (len g) by A13, FINSEQ_1:def 7;
then g . (len g) <= x1 by A11, A14, A15, A16, A19, A21, VALUED_0:def 13, INT_1:52;
then (g . (len g)) ! divides x1 ! by Th6;
then A29: ((g . (len g)) !) * x divides (x1 !) * x by NAT_3:1;
A30: (x1 + 1) ! = (x1 !) * (x1 + 1) by NEWTON:15;
Product f = (Product g) * x by A13, RVSUM_1:96;
hence Product f divides (f . (len f)) ! by A15, A28, A29, A30, INT_2:9; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
then A31: Product f divides (f . (len f)) ! by A1, A2, A3, A4;
0 + 1 <= len f by A4, NAT_1:13;
then len f in dom f by FINSEQ_3:25;
then (f . (len f)) ! divides n ! by A1, Th6;
hence Product f divides n ! by A31, INT_2:9; :: thesis: verum

end;

end;