let n be Nat; :: thesis:
let p be Prime; :: thesis:
assume A1: ( p <= n & p |^ 2 divides n ! & 2 * p > n ) ; :: thesis:
p |^ (1 + 1) = p * (p |^ 1) by NEWTON:6;
then consider o being Nat such that
A2: (p * p) * o = n ! by A1, NAT_D:def 3;
set I = idseq n;
for r being Real st r in rng (idseq n) holds
0 < r

let r be Real; :: thesis:
assume r in rng (idseq n) ; :: thesis:
then consider x being object such that
A3: ( x in dom (idseq n) & (idseq n) . x = r ) by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
idseq n = id (Seg n) by FINSEQ_2:def 1;
then r = x by A3, FINSEQ_2:49;
hence 0 < r by A3, FINSEQ_3:25; :: thesis:

end;

then A4: idseq n is positive-yielding by PARTFUN3:def 1;
A5: ( 1 < p & p <= len (idseq n) ) by A1, INT_2:def 4;
then A6: idseq n = (((idseq n) | (p -' 1)) ^ <*((idseq n) . p)*>) ^ ((idseq n) /^ p) by FINSEQ_5:84;
then A7: Product (idseq n) = (Product (((idseq n) | (p -' 1)) ^ <*((idseq n) . p)*>)) * (Product ((idseq n) /^ p)) by RVSUM_1:97
.= ((Product ((idseq n) | (p -' 1))) * ((idseq n) . p)) * (Product ((idseq n) /^ p)) by RVSUM_1:96
.= ((Product ((idseq n) | (p -' 1))) * (Product ((idseq n) /^ p))) * ((idseq n) . p)
.= (Product (((idseq n) | (p -' 1)) ^ ((idseq n) /^ p))) * ((idseq n) . p) by RVSUM_1:97 ;
p in Seg n by A5;
then A8: (idseq n) . p = p by FINSEQ_2:49;
A9: ( ((idseq n) | (p -' 1)) ^ <*((idseq n) . p)*> is positive-yielding & (idseq n) /^ p is positive-yielding ) by A4, A6, NUMBER08:37;
then (idseq n) | (p -' 1) is positive-yielding by NUMBER08:37;
then A10: ((idseq n) | (p -' 1)) ^ ((idseq n) /^ p) is positive-yielding by A9;
Product (idseq n) = n ! by NEWTON:def 2;
then (p * p) * o = Product (idseq n) by A2;
then p * (p * o) = (Product (((idseq n) | (p -' 1)) ^ ((idseq n) /^ p))) * p by A7, A8;
then p * o = Product (((idseq n) | (p -' 1)) ^ ((idseq n) /^ p)) by XCMPLX_1:5;
then A11: p divides Product (((idseq n) | (p -' 1)) ^ ((idseq n) /^ p)) ;
rng (((idseq n) | (p -' 1)) ^ ((idseq n) /^ p)) c= NAT ;
then ((idseq n) | (p -' 1)) ^ ((idseq n) /^ p) is FinSequence of NAT by FINSEQ_1:def 4;
then consider i being Nat such that
A12: i in dom (((idseq n) | (p -' 1)) ^ ((idseq n) /^ p)) and
A13: p divides (((idseq n) | (p -' 1)) ^ ((idseq n) /^ p)) . i by A11, A10, HILB10_5:3;
1 < p by A5;
then A14: p -' 1 = p - 1 by XREAL_1:233;
then p -' 1 < p - 0 by XREAL_1:15;
then A15: p -' 1 < len (idseq n) by A5, XXREAL_0:2;
then A16: len ((idseq n) | (p -' 1)) = p -' 1 by FINSEQ_1:59;

per cases by A12, FINSEQ_1:25;

suppose A17: i in dom ((idseq n) | (p -' 1)) ; :: thesis:

then A18: (((idseq n) | (p -' 1)) ^ ((idseq n) /^ p)) . i = ((idseq n) | (p -' 1)) . i by FINSEQ_1:def 7
.= (idseq n) . i by FUNCT_1:47, A17 ;
A19: ( 1 <= i & i <= p -' 1 ) by A16, A17, FINSEQ_3:25;
then i <= len (idseq n) by A15, XXREAL_0:2;
then i in Seg n by A19;
then (idseq n) . i = i by FINSEQ_2:49;
then p divides i by A18, A13;
then ( (p -' 1) + 1 = p & p <= i ) by A14, A19, INT_2:27;
hence contradiction by A19, NAT_1:13; :: thesis:

end;

suppose ex k being Nat st
( k in dom ((idseq n) /^ p) & i = (len ((idseq n) | (p -' 1))) + k ) ; :: thesis:

then consider k being Nat such that
A20: ( k in dom ((idseq n) /^ p) & i = (len ((idseq n) | (p -' 1))) + k ) ;
k + p in dom (idseq n) by A20, FINSEQ_5:26;
then A21: k + p in Seg n by A6, FINSEQ_1:def 3;
(((idseq n) | (p -' 1)) ^ ((idseq n) /^ p)) . i = ((idseq n) /^ p) . k by A20, FINSEQ_1:def 7
.= (idseq n) . (k + p) by A20, A5, RFINSEQ:def 1
.= k + p by A21, FINSEQ_2:49 ;
then p divides k + p by A13;
then consider o being Nat such that
A22: p * o = k + p by NAT_D:def 3;
o <> 0 by A22;
then A23: o >= 1 by NAT_1:14;
1 <= k by A20, FINSEQ_3:25;
then k <> 0 ;
then o <> 1 by A22;
then o > 1 by A23, XXREAL_0:1;
then o >= 1 + 1 by NAT_1:13;
then k + p >= 2 * p by A22, XREAL_1:66;
then k + p > n by A1, XXREAL_0:2;
hence contradiction by A21, FINSEQ_1:1; :: thesis:

end;

end;