set g = XFS2FS f;
let e1, e2 be ExtReal; VALUED_0:def 14 ( not e1 in proj1 (XFS2FS f) or not e2 in proj1 (XFS2FS f) or e2 <= e1 or not (XFS2FS f) . e1 <= (XFS2FS f) . e2 )
assume that
A1:
e1 in dom (XFS2FS f)
and
A2:
e2 in dom (XFS2FS f)
and
A3:
e1 < e2
; not (XFS2FS f) . e1 <= (XFS2FS f) . e2
A4:
1 <= e1
by A1, FINSEQ_3:25;
A5:
1 <= e2
by A2, FINSEQ_3:25;
reconsider e1 = e1, e2 = e2 as non zero Nat by A1, A2, FINSEQ_3:25;
A6:
len (XFS2FS f) = len f
by AFINSQ_1:def 9;
e1 <= len (XFS2FS f)
by A1, FINSEQ_3:25;
then A7:
f . (e1 - 1) = (XFS2FS f) . e1
by A4, A6, AFINSQ_1:def 9;
e2 <= len (XFS2FS f)
by A2, FINSEQ_3:25;
then A8:
f . (e2 - 1) = (XFS2FS f) . e2
by A5, A6, AFINSQ_1:def 9;
A9:
e1 - 1 < e2 - 1
by A3, XREAL_1:8;
( e1 - 1 in dom f & e2 - 1 in dom f )
by A1, A2, Th1;
hence
not (XFS2FS f) . e1 <= (XFS2FS f) . e2
by A7, A8, A9, VALUED_0:def 14; verum