let n be Nat; for f being Element of REAL * ex i being Nat st
( i <= n & OuterVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n) = {} )
let f be Element of REAL * ; ex i being Nat st
( i <= n & OuterVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n) = {} )
set R = Relax n;
set M = findmin n;
defpred S1[ Nat] means ( $1 <= n implies card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . $1) . f),n)) <= n - $1 );
set nf = ((repeat ((Relax n) * (findmin n))) . n) . f;
assume A1:
for i being Nat holds
( not i <= n or not OuterVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n) = {} )
; contradiction
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
now ( k + 1 <= n implies card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)) <= n - (k + 1) )set fk =
UnusedVx (
(((repeat ((Relax n) * (findmin n))) . k) . f),
n);
set fk1 =
UnusedVx (
(((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),
n);
A4:
k <= k + 1
by NAT_1:11;
assume A5:
k + 1
<= n
;
card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)) <= n - (k + 1)then
OuterVx (
(((repeat ((Relax n) * (findmin n))) . k) . f),
n)
<> {}
by A1, A4, XXREAL_0:2;
then
UnusedVx (
(((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),
n)
c< UnusedVx (
(((repeat ((Relax n) * (findmin n))) . k) . f),
n)
by Th38;
then
card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)) < n - k
by A3, A5, A4, CARD_2:48, XXREAL_0:2;
then
(card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n))) + 1
<= n - k
by INT_1:7;
then
card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)) <= (n - k) - 1
by XREAL_1:19;
hence
card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)) <= n - (k + 1)
;
verum end;
hence
S1[
k + 1]
;
verum
end;
A6:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A6, A2);
then
S1[n]
;
then A7:
UnusedVx ((((repeat ((Relax n) * (findmin n))) . n) . f),n) = {}
;
OuterVx ((((repeat ((Relax n) * (findmin n))) . n) . f),n) c= UnusedVx ((((repeat ((Relax n) * (findmin n))) . n) . f),n)
by Th27;
hence
contradiction
by A1, A7, XBOOLE_1:3; verum