let n be Nat; :: thesis: 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 * ; :: thesis: 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) = {} ) ; :: thesis: contradiction
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( 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 ; :: thesis: 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) ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A6: S1[ 0 ]
proof
set f0 = ((repeat ((Relax n) * (findmin n))) . 0) . f;
assume 0 <= n ; :: thesis: card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n)) <= n - 0
card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n)) <= card (Seg n) by Th26, NAT_1:43;
hence card (UnusedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n)) <= n - 0 by FINSEQ_1:57; :: thesis: verum
end;
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; :: thesis: verum