let G be real-weighted WGraph; :: thesis: for src being Vertex of G
for i, j being Nat st i <= j holds
( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . j) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . j) `2 )
let src be Vertex of G; :: thesis: for i, j being Nat st i <= j holds
( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . j) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . j) `2 )
let i, j be Nat; :: thesis: ( i <= j implies ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . j) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . j) `2 ) )
set DCS = DIJK:CompSeq src;
set dDCS = dom (((DIJK:CompSeq src) . i) `1);
set eDCS = ((DIJK:CompSeq src) . i) `2 ;
defpred S₁[ Nat] means ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . (i + $1)) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . (i + $1)) `2 );
assume i <= j ; :: thesis: ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . j) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . j) `2 )
then A1: ex x being Nat st j = i + x by NAT_1:10;

now :: thesis: for k being Nat st dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . (i + k)) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . (i + k)) `2 holds
( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . (i + (k + 1))) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . (i + (k + 1))) `2 )

let k be Nat; :: thesis: ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . (i + k)) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . (i + k)) `2 implies ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . (i + (k + 1))) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . (i + (k + 1))) `2 ) )
(DIJK:CompSeq src) . ((i + k) + 1) = DIJK:Step ((DIJK:CompSeq src) . (i + k)) by Def11;
then A2: ( dom (((DIJK:CompSeq src) . (i + k)) `1) c= dom (((DIJK:CompSeq src) . ((i + k) + 1)) `1) & ((DIJK:CompSeq src) . (i + k)) `2 c= ((DIJK:CompSeq src) . ((i + k) + 1)) `2 ) by Th16;
assume ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . (i + k)) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . (i + k)) `2 ) ; :: thesis: ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . (i + (k + 1))) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . (i + (k + 1))) `2 )
hence ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . (i + (k + 1))) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . (i + (k + 1))) `2 ) by A2; :: thesis: verum

end;

then A3: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A4: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A3);
hence ( dom (((DIJK:CompSeq src) . i) `1) c= dom (((DIJK:CompSeq src) . j) `1) & ((DIJK:CompSeq src) . i) `2 c= ((DIJK:CompSeq src) . j) `2 ) by A1; :: thesis: verum