let n be Element of NAT ; :: thesis: for f being Element of REAL * ex i being Element of NAT st
( i <= n & OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n = {} )
let f be Element of REAL * ; :: thesis: ex i being Element of NAT st
( i <= n & OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n = {} )
set R = Relax n;
set M = findmin n;
assume A1: for i being Element of NAT holds
( not i <= n or not OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n = {} ) ; :: thesis: contradiction
defpred S₁[ Element of NAT ] means ( $1 <= n implies card (UnusedVx (((repeat ((Relax n) * (findmin n))) . $1) . f),n) <= n - $1 );
A2: S₁[ 0 ]

proof

assume 0 <= n ; :: thesis: card (UnusedVx (((repeat ((Relax n) * (findmin n))) . 0 ) . f),n) <= n - 0
set f0 = ((repeat ((Relax n) * (findmin n))) . 0 ) . f;
card (UnusedVx (((repeat ((Relax n) * (findmin n))) . 0 ) . f),n) <= card (Seg n) by Th27, NAT_1:44;
hence card (UnusedVx (((repeat ((Relax n) * (findmin n))) . 0 ) . f),n) <= n - 0 by FINSEQ_1:78; :: thesis: verum

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now

assume A5: k + 1 <= n ; :: thesis: card (UnusedVx (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) <= n - (k + 1)
A6: k <= k + 1 by NAT_1:11;
set fk = UnusedVx (((repeat ((Relax n) * (findmin n))) . k) . f),n;
set fk1 = UnusedVx (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n;
OuterVx (((repeat ((Relax n) * (findmin n))) . k) . f),n <> {} by A1, A5, A6, 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 Th39;
then card (UnusedVx (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) < card (UnusedVx (((repeat ((Relax n) * (findmin n))) . k) . f),n) by CARD_2:67;
then card (UnusedVx (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) < n - k by A4, A5, A6, XXREAL_0:2;
then (card (UnusedVx (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n)) + 1 <= n - k by INT_1:20;
then card (UnusedVx (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) <= (n - k) - 1 by XREAL_1:21;
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;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
then A7: S₁[n] ;
set nf = ((repeat ((Relax n) * (findmin n))) . n) . f;
card (UnusedVx (((repeat ((Relax n) * (findmin n))) . n) . f),n) = 0 by A7;
then A8: 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 Th28;
hence contradiction by A1, A8, XBOOLE_1:3; :: thesis: verum