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 S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[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 S₁[k + 1] ; :: thesis: verum

end;

A6: S₁[ 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 S₁[k] from NAT_1:sch 2(A6, A2);
then S₁[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