let G be finite real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for source being Vertex of G holds source in dom (AP:FindAugPath EL,source)
let EL be FF:ELabeling of G; :: thesis: for source being Vertex of G holds source in dom (AP:FindAugPath EL,source)
let source be Vertex of G; :: thesis: source in dom (AP:FindAugPath EL,source)
set CS = AP:CompSeq EL,source;
set V = AP:FindAugPath EL,source;
dom ((AP:CompSeq EL,source) . 0 ) = {source} by Th3;
then A1: source in dom ((AP:CompSeq EL,source) . 0 ) by TARSKI:def 1;
dom ((AP:CompSeq EL,source) . 0 ) c= dom (AP:FindAugPath EL,source) by Th4;
hence source in dom (AP:FindAugPath EL,source) by A1; :: thesis: verum