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