let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for source being Vertex of G
for i, j being Nat st i <= j holds
dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
let EL be FF:ELabeling of G; :: thesis: for source being Vertex of G
for i, j being Nat st i <= j holds
dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
let source be Vertex of G; :: thesis: for i, j being Nat st i <= j holds
dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
let i, j be Nat; :: thesis: ( i <= j implies dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j) )
set CS = AP:CompSeq (EL,source);
defpred S₁[ Nat] means dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . (i + $1));
assume i <= j ; :: thesis: dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
then consider k being Nat such that
A1: j = i + k by NAT_1:10;

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set Gn = (AP:CompSeq (EL,source)) . (i + n);
set Gn1 = (AP:CompSeq (EL,source)) . (i + (n + 1));
set Next = AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n));
set e = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n));
(AP:CompSeq (EL,source)) . (i + (n + 1)) = (AP:CompSeq (EL,source)) . ((i + n) + 1) ;
then A3: (AP:CompSeq (EL,source)) . (i + (n + 1)) = AP:Step ((AP:CompSeq (EL,source)) . (i + n)) by Def12;
assume A4: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: S₁[n + 1]

per cases ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) = {} or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) in dom ((AP:CompSeq (EL,source)) . (i + n)) ) or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) in dom ((AP:CompSeq (EL,source)) . (i + n)) ) ) ;

suppose AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) = {} ; :: thesis: S₁[n + 1]

hence S₁[n + 1] by A4, A3, Def10; :: thesis: verum

end;

suppose ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) in dom ((AP:CompSeq (EL,source)) . (i + n)) ) ; :: thesis: S₁[n + 1]

then (AP:CompSeq (EL,source)) . (i + (n + 1)) = ((AP:CompSeq (EL,source)) . (i + n)) +* (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n))) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n))) by A3, Def10;
then dom ((AP:CompSeq (EL,source)) . (i + n)) c= dom ((AP:CompSeq (EL,source)) . (i + (n + 1))) by FUNCT_4:10;
hence S₁[n + 1] by A4, XBOOLE_1:1; :: thesis: verum

end;

suppose ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) in dom ((AP:CompSeq (EL,source)) . (i + n)) ) ; :: thesis: S₁[n + 1]

then (AP:CompSeq (EL,source)) . (i + (n + 1)) = ((AP:CompSeq (EL,source)) . (i + n)) +* (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n))) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n))) by A3, Def10;
then dom ((AP:CompSeq (EL,source)) . (i + n)) c= dom ((AP:CompSeq (EL,source)) . (i + (n + 1))) by FUNCT_4:10;
hence S₁[n + 1] by A4, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A5: S₁[ 0 ] ;
A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A2);
thus dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j) by A6, A1; :: thesis: verum