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} ; :: thesis: verum