let n, i be Element of NAT ; :: thesis: for f being Element of REAL * st OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n <> {} holds
UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n c< UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n
let f be Element of REAL * ; :: thesis: ( OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n <> {} implies UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n c< UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n )
set R = Relax n;
set M = findmin n;
set ff = ((repeat ((Relax n) * (findmin n))) . i) . f;
set Fi1 = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f;
assume OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n <> {} ; :: thesis: UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n c< UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n
then A1: ex j being Element of NAT st
( j in OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n & 1 <= j & j <= n & ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . j = - 1 ) by Th35;
A2: dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) = dom (((repeat ((Relax n) * (findmin n))) . i) . f) by Th38
.= dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) by Th34 ;

A3: now

let x be set ; :: thesis: ( x in UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n implies ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . x <> - 1 )
assume x in UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n ; :: thesis: ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . x <> - 1
then consider k being Element of NAT such that
A4: x = k and
A5: k in dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) and
1 <= k and
A6: k <= n and
A7: (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k <> - 1 ;
(((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . k by Th23
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k by A2, A5, A6, Th37 ;
hence ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . x <> - 1 by A4, A7; :: thesis: verum

end;

A8: UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n c= UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n

proof

A9: n < ((n * n) + (3 * n)) + 1 by Lm7;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n or x in UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n )
assume x in UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n ; :: thesis: x in UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n
then consider k being Element of NAT such that
A10: x = k and
A11: k in dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) and
A12: 1 <= k and
A13: k <= n and
A14: (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k <> - 1 ;
A15: k in dom (((repeat ((Relax n) * (findmin n))) . i) . f) by A11, Th38;
(((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . k by Th23
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k by A2, A11, A13, Th37 ;
then (((repeat ((Relax n) * (findmin n))) . i) . f) . k <> - 1 by A13, A14, A15, A9, Th33;
hence x in UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n by A10, A12, A13, A15; :: thesis: verum

end;

OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n c= UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n by Th28;
then UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n <> UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n by A1, A3;
hence UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n c< UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n by A8, XBOOLE_0:def 8; :: thesis: verum