let n be Element of NAT ; :: thesis: for f being Element of REAL * holds dom ((findmin n) . f) = dom f
let f be Element of REAL * ; :: thesis: dom ((findmin n) . f) = dom f
(findmin n) . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) by Def11;
hence dom ((findmin n) . f) = dom f by Th21; :: thesis: verum