set g = XFS2FS f;
let e1, e2 be ExtReal; VALUED_0:def 16 ( not e1 in proj1 (XFS2FS f) or not e2 in proj1 (XFS2FS f) or not e1 <= e2 or (XFS2FS f) . e2 <= (XFS2FS f) . e1 )
assume that
A1:
e1 in dom (XFS2FS f)
and
A2:
e2 in dom (XFS2FS f)
and
A3:
e1 <= e2
; (XFS2FS f) . e2 <= (XFS2FS f) . e1
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;
( e1 - 1 in dom f & e2 - 1 in dom f )
by A1, A2, Th1;
hence
(XFS2FS f) . e2 <= (XFS2FS f) . e1
by A3, A7, A8, VALUED_0:def 16, XREAL_1:6; verum