let n be 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)),(- jj)) by Def11;
hence dom ((findmin n) . f) = dom f by Th20; :: thesis: verum