let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for source being Vertex of G holds dom ((AP:CompSeq EL,source) . 0 ) = {source}
let EL be FF:ELabeling of G; :: thesis: for source being Vertex of G holds dom ((AP:CompSeq EL,source) . 0 ) = {source}
let source be Vertex of G; :: thesis: dom ((AP:CompSeq EL,source) . 0 ) = {source}
(AP:CompSeq EL,source) . 0 = source .--> 1 by Def12;
hence dom ((AP:CompSeq EL,source) . 0 ) = {source} by FUNCOP_1:19; :: thesis: verum