now :: thesis: for x1, x2 being object st x1 in dom (XFS2FS p) & x2 in dom (XFS2FS p) & (XFS2FS p) . x1 = (XFS2FS p) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (XFS2FS p) & x2 in dom (XFS2FS p) & (XFS2FS p) . x1 = (XFS2FS p) . x2 implies x1 = x2 )
assume that
A1: ( x1 in dom (XFS2FS p) & x2 in dom (XFS2FS p) ) and
A2: (XFS2FS p) . x1 = (XFS2FS p) . x2 ; :: thesis: x1 = x2
reconsider n1 = x1, n2 = x2 as Nat by A1;
( 1 <= n1 & n1 <= len (XFS2FS p) & 1 <= n2 & n2 <= len (XFS2FS p) ) by A1, FINSEQ_3:25;
then A3: ( 1 <= n1 & n1 <= len p & 1 <= n2 & n2 <= len p ) by Def9A;
then A4: ( p . (n1 - 1) = (XFS2FS p) . n1 & p . (n2 - 1) = (XFS2FS p) . n2 ) by Def9A;
A5: ( (n1 -' 1) + 1 = n1 & (n2 -' 1) + 1 = n2 ) by A3, XREAL_1:235;
then ( n1 -' 1 in dom p & n2 -' 1 in dom p ) by A1, Th14;
hence x1 = x2 by A2, A4, A5, FUNCT_1:def 4; :: thesis: verum

end;

hence XFS2FS p is one-to-one ; :: thesis: verum