let G be real-weighted WGraph; :: thesis: for src being Vertex of G holds dom ((DIJK:Init src) `1) = {src}
let src be Vertex of G; :: thesis: dom ((DIJK:Init src) `1) = {src}
set G2 = DIJK:Init src;
(DIJK:Init src) `1 = src .--> 0 by MCART_1:7;
hence dom ((DIJK:Init src) `1) = {src} by FUNCOP_1:13; :: thesis: verum