let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of
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 ; :: 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;
assume A1: i <= j ; :: thesis: dom ((AP:CompSeq EL,source) . i) c= dom ((AP:CompSeq EL,source) . j)
defpred S₁[ Element of NAT ] means dom ((AP:CompSeq EL,source) . i) c= dom ((AP:CompSeq EL,source) . (i + $1));
A2: S₁[ 0 ] ;

A3: now

let n be Element of 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 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (i + n)));
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
(AP:CompSeq EL,source) . (i + (n + 1)) = (AP:CompSeq EL,source) . ((i + n) + 1) ;
then A5: (AP:CompSeq EL,source) . (i + (n + 1)) = AP:Step ((AP:CompSeq EL,source) . (i + n)) by Def15;

now

per cases ( AP:NextBestEdges ((AP:CompSeq EL,source) . (i + n)) = {} or ( AP:NextBestEdges ((AP:CompSeq EL,source) . (i + n)) <> {} & not (the_Source_of G) . (choose (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) . (choose (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, A5, Def14; :: thesis: verum

end;

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

(AP:CompSeq EL,source) . (i + (n + 1)) = ((AP:CompSeq EL,source) . (i + n)) +* (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (i + n))))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (i + n))))) by A5, A6, Def14;
then dom ((AP:CompSeq EL,source) . (i + n)) c= dom ((AP:CompSeq EL,source) . (i + (n + 1))) by FUNCT_4:11;
hence S₁[n + 1] by A4, XBOOLE_1:1; :: thesis: verum

end;

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

(AP:CompSeq EL,source) . (i + (n + 1)) = ((AP:CompSeq EL,source) . (i + n)) +* (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (i + n))))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (i + n))))) by A5, A8, Def14;
then dom ((AP:CompSeq EL,source) . (i + n)) c= dom ((AP:CompSeq EL,source) . (i + (n + 1))) by FUNCT_4:11;
hence S₁[n + 1] by A4, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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

end;

A10: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
consider k being Nat such that
A11: j = i + k by A1, NAT_1:10;
k in NAT by ORDINAL1:def 13;
hence dom ((AP:CompSeq EL,source) . i) c= dom ((AP:CompSeq EL,source) . j) by A10, A11; :: thesis: verum