let n be Nat; :: thesis: for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds

(Y_axis f) . m <= (Y_axis f) . n ) holds

f /. n in rng (Col ((GoB f),(width (GoB f))))

let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( n in dom f & ( for m being Nat st m in dom f holds

(Y_axis f) . m <= (Y_axis f) . n ) implies f /. n in rng (Col ((GoB f),(width (GoB f)))) )

set x = X_axis f;

set y = Y_axis f;

set r = (Y_axis f) . n;

assume that

A1: n in dom f and

A2: for m being Nat st m in dom f holds

(Y_axis f) . m <= (Y_axis f) . n ; :: thesis: f /. n in rng (Col ((GoB f),(width (GoB f))))

reconsider p = f /. n as Point of (TOP-REAL 2) ;

A3: dom f = Seg (len f) by FINSEQ_1:def 3;

A4: ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def 3, GOBOARD1:def 2;

then A5: (Y_axis f) . n = p `2 by A1, A3, GOBOARD1:def 2;

A6: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def 21;

(Y_axis f) . n in rng (Y_axis f) by A1, A3, A4, FUNCT_1:def 3;

then consider j being Nat such that

A7: j in dom (Incr (Y_axis f)) and

A8: (Incr (Y_axis f)) . j = p `2 by A5, A6, FINSEQ_2:10;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A9: j <= len (Incr (Y_axis f)) by A7, FINSEQ_3:25;

A10: 1 <= j by A7, FINSEQ_3:25;

( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def 3, GOBOARD1:def 1;

then ( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) ) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 1;

then consider i being Nat such that

A16: i in dom (Incr (X_axis f)) and

A17: (Incr (X_axis f)) . i = p `1 by A15, FINSEQ_2:10;

A18: p = |[(p `1),(p `2)]| by EUCLID:53;

len (Col ((GoB f),(width (GoB f)))) = len (GoB f) by MATRIX_0:def 8;

then A19: dom (Col ((GoB f),(width (GoB f)))) = dom (GoB f) by FINSEQ_3:29;

( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def 21;

then A20: dom (Incr (X_axis f)) = dom (GoB f) by FINSEQ_3:29;

A21: ( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def 21;

then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (Y_axis f)) = Seg (width (GoB f)) ) by FINSEQ_1:def 3, MATRIX_0:def 4;

then [i,(width (GoB f))] in Indices (GoB f) by A21, A16, A7, A20, A11, ZFMISC_1:87;

then (GoB f) * (i,(width (GoB f))) = |[(p `1),(p `2)]| by A21, A17, A8, A11, Def1;

then (Col ((GoB f),(width (GoB f)))) . i = f /. n by A16, A20, A18, MATRIX_0:def 8;

hence f /. n in rng (Col ((GoB f),(width (GoB f)))) by A16, A20, A19, FUNCT_1:def 3; :: thesis: verum

(Y_axis f) . m <= (Y_axis f) . n ) holds

f /. n in rng (Col ((GoB f),(width (GoB f))))

let f be non empty FinSequence of (TOP-REAL 2); :: thesis: ( n in dom f & ( for m being Nat st m in dom f holds

(Y_axis f) . m <= (Y_axis f) . n ) implies f /. n in rng (Col ((GoB f),(width (GoB f)))) )

set x = X_axis f;

set y = Y_axis f;

set r = (Y_axis f) . n;

assume that

A1: n in dom f and

A2: for m being Nat st m in dom f holds

(Y_axis f) . m <= (Y_axis f) . n ; :: thesis: f /. n in rng (Col ((GoB f),(width (GoB f))))

reconsider p = f /. n as Point of (TOP-REAL 2) ;

A3: dom f = Seg (len f) by FINSEQ_1:def 3;

A4: ( dom (Y_axis f) = Seg (len (Y_axis f)) & len (Y_axis f) = len f ) by FINSEQ_1:def 3, GOBOARD1:def 2;

then A5: (Y_axis f) . n = p `2 by A1, A3, GOBOARD1:def 2;

A6: rng (Incr (Y_axis f)) = rng (Y_axis f) by SEQ_4:def 21;

(Y_axis f) . n in rng (Y_axis f) by A1, A3, A4, FUNCT_1:def 3;

then consider j being Nat such that

A7: j in dom (Incr (Y_axis f)) and

A8: (Incr (Y_axis f)) . j = p `2 by A5, A6, FINSEQ_2:10;

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A9: j <= len (Incr (Y_axis f)) by A7, FINSEQ_3:25;

A10: 1 <= j by A7, FINSEQ_3:25;

A11: now :: thesis: not j <> len (Incr (Y_axis f))

A15:
rng (Incr (X_axis f)) = rng (X_axis f)
by SEQ_4:def 21;reconsider s = (Incr (Y_axis f)) . (j + 1) as Real ;

assume j <> len (Incr (Y_axis f)) ; :: thesis: contradiction

then j < len (Incr (Y_axis f)) by A9, XXREAL_0:1;

then A12: j + 1 <= len (Incr (Y_axis f)) by NAT_1:13;

1 <= j + 1 by A10, NAT_1:13;

then A13: j + 1 in dom (Incr (Y_axis f)) by A12, FINSEQ_3:25;

then (Incr (Y_axis f)) . (j + 1) in rng (Incr (Y_axis f)) by FUNCT_1:def 3;

then A14: ex m being Nat st

( m in dom (Y_axis f) & (Y_axis f) . m = s ) by A6, FINSEQ_2:10;

j < j + 1 by NAT_1:13;

then (Y_axis f) . n < s by A5, A7, A8, A13, SEQM_3:def 1;

hence contradiction by A2, A3, A4, A14; :: thesis: verum

end;assume j <> len (Incr (Y_axis f)) ; :: thesis: contradiction

then j < len (Incr (Y_axis f)) by A9, XXREAL_0:1;

then A12: j + 1 <= len (Incr (Y_axis f)) by NAT_1:13;

1 <= j + 1 by A10, NAT_1:13;

then A13: j + 1 in dom (Incr (Y_axis f)) by A12, FINSEQ_3:25;

then (Incr (Y_axis f)) . (j + 1) in rng (Incr (Y_axis f)) by FUNCT_1:def 3;

then A14: ex m being Nat st

( m in dom (Y_axis f) & (Y_axis f) . m = s ) by A6, FINSEQ_2:10;

j < j + 1 by NAT_1:13;

then (Y_axis f) . n < s by A5, A7, A8, A13, SEQM_3:def 1;

hence contradiction by A2, A3, A4, A14; :: thesis: verum

( dom (X_axis f) = Seg (len (X_axis f)) & len (X_axis f) = len f ) by FINSEQ_1:def 3, GOBOARD1:def 1;

then ( (X_axis f) . n = p `1 & (X_axis f) . n in rng (X_axis f) ) by A1, A3, FUNCT_1:def 3, GOBOARD1:def 1;

then consider i being Nat such that

A16: i in dom (Incr (X_axis f)) and

A17: (Incr (X_axis f)) . i = p `1 by A15, FINSEQ_2:10;

A18: p = |[(p `1),(p `2)]| by EUCLID:53;

len (Col ((GoB f),(width (GoB f)))) = len (GoB f) by MATRIX_0:def 8;

then A19: dom (Col ((GoB f),(width (GoB f)))) = dom (GoB f) by FINSEQ_3:29;

( len (GoB f) = card (rng (X_axis f)) & len (Incr (X_axis f)) = card (rng (X_axis f)) ) by Th13, SEQ_4:def 21;

then A20: dom (Incr (X_axis f)) = dom (GoB f) by FINSEQ_3:29;

A21: ( width (GoB f) = card (rng (Y_axis f)) & len (Incr (Y_axis f)) = card (rng (Y_axis f)) ) by Th13, SEQ_4:def 21;

then ( Indices (GoB f) = [:(dom (GoB f)),(Seg (width (GoB f))):] & dom (Incr (Y_axis f)) = Seg (width (GoB f)) ) by FINSEQ_1:def 3, MATRIX_0:def 4;

then [i,(width (GoB f))] in Indices (GoB f) by A21, A16, A7, A20, A11, ZFMISC_1:87;

then (GoB f) * (i,(width (GoB f))) = |[(p `1),(p `2)]| by A21, A17, A8, A11, Def1;

then (Col ((GoB f),(width (GoB f)))) . i = f /. n by A16, A20, A18, MATRIX_0:def 8;

hence f /. n in rng (Col ((GoB f),(width (GoB f)))) by A16, A20, A19, FUNCT_1:def 3; :: thesis: verum