let G be _finite real-weighted WGraph; :: thesis: for i, j being Nat st i <= j holds
( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 )
let i, j be Nat; :: thesis: ( i <= j implies ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 ) )
set PCS = PRIM:CompSeq G;
set vPCS = ((PRIM:CompSeq G) . i) `1 ;
set ePCS = ((PRIM:CompSeq G) . i) `2 ;
defpred S1[ Nat] means ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + $1)) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + $1)) `2 );
assume i <= j ; :: thesis: ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 )
then A1: ex x being Nat st j = i + x by NAT_1:10;
now :: thesis: for k being Nat st ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + k)) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + k)) `2 holds
( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + (k + 1))) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + (k + 1))) `2 )
let k be Nat; :: thesis: ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + k)) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + k)) `2 implies ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + (k + 1))) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + (k + 1))) `2 ) )
(PRIM:CompSeq G) . ((i + k) + 1) = PRIM:Step ((PRIM:CompSeq G) . (i + k)) by Def17;
then A2: ( ((PRIM:CompSeq G) . (i + k)) `1 c= ((PRIM:CompSeq G) . ((i + k) + 1)) `1 & ((PRIM:CompSeq G) . (i + k)) `2 c= ((PRIM:CompSeq G) . ((i + k) + 1)) `2 ) by Th29;
assume ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + k)) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + k)) `2 ) ; :: thesis: ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + (k + 1))) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + (k + 1))) `2 )
hence ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . (i + (k + 1))) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . (i + (k + 1))) `2 ) by A2; :: thesis: verum
end;
then A3: for k being Nat st S1[k] holds
S1[k + 1] ;
A4: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A3);
 hence ( ((PRIM:CompSeq G) . i) `1 c= ((PRIM:CompSeq G) . j) `1 & ((PRIM:CompSeq G) . i) `2 c= ((PRIM:CompSeq G) . j) `2 ) by A1; :: thesis: verum