let i, n be 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 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 Th34;
A2: dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) = dom (((repeat ((Relax n) * (findmin n))) . i) . f) by Th37
.= dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) by Th33 ;
A3: now :: thesis: for x being set st x in UnusedVx ((((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n) holds
((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . x <> - 1
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 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 Th22
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k by A2, A5, A6, Th36 ;
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 object ; :: 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 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, Th37;
(((repeat ((Relax n) * (findmin n))) . (i + 1)) . f) . k = ((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . k by Th22
.= ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k by A2, A11, A13, Th36 ;
then (((repeat ((Relax n) * (findmin n))) . i) . f) . k <> - 1 by A13, A14, A15, A9, Th32;
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 Th27;
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