let a, b, n be Nat; :: thesis: ( 0 < a & a < b & b <= n implies a * b divides n ! )
assume A1: ( 0 < a & a < b & b <= n ) ; :: thesis: a * b divides n !
A2: for x being object st x in dom <*a,b*> holds
<*a,b*> . x <= n

proof

let x be object ; :: thesis: ( x in dom <*a,b*> implies <*a,b*> . x <= n )
assume A3: x in dom <*a,b*> ; :: thesis: <*a,b*> . x <= n
len <*a,b*> = 2 by FINSEQ_1:44;
then dom <*a,b*> = Seg 2 by FINSEQ_1:def 3;
then ( x = 1 or x = 2 ) by A3, FINSEQ_1:2, TARSKI:def 2;
hence <*a,b*> . x <= n by A1, XXREAL_0:2; :: thesis: verum

end;

rng <*a*> c= NAT ;
then A4: <*a*> is FinSequence of NAT by FINSEQ_1:def 4;
for i being Nat st i in dom <*a*> holds
<*a*> . i < b

proof

let i be Nat; :: thesis: ( i in dom <*a*> implies <*a*> . i < b )
assume i in dom <*a*> ; :: thesis: <*a*> . i < b
then i in Seg 1 by FINSEQ_1:38;
then i = 1 by FINSEQ_1:2, TARSKI:def 1;
hence <*a*> . i < b by A1; :: thesis: verum

end;

then A5: ( <*a,b*> is increasing & <*a,b*> is positive-yielding ) by A1, A4, NUMBER12:8;
Product <*a,b*> = (Product <*a*>) * b by RVSUM_1:96
.= a * b ;
hence a * b divides n ! by A2, A5, NUMBER08:def 4, NUMBER08:38; :: thesis: verum