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

let x1, x2 be object ; :: thesis: ( x1 in dom (FS2XFS p) & x2 in dom (FS2XFS p) & (FS2XFS p) . x1 = (FS2XFS p) . x2 implies x1 = x2 )
assume that
A1: ( x1 in dom (FS2XFS p) & x2 in dom (FS2XFS p) ) and
A2: (FS2XFS p) . x1 = (FS2XFS p) . x2 ; :: thesis: x1 = x2
reconsider n1 = x1, n2 = x2 as Nat by A1;
A3: ( n1 + 1 in dom p & n2 + 1 in dom p ) by A1, Th13;
then ( n1 + 1 <= len p & n2 + 1 <= len p ) by FINSEQ_3:25;
then A4: ( n1 < len p & n2 < len p ) by NAT_1:13;
p . (n1 + 1) = (FS2XFS p) . n1 by A4, Def8
.= p . (n2 + 1) by A2, A4, Def8 ;
then n1 + 1 = n2 + 1 by A3, FUNCT_1:def 4;
hence x1 = x2 ; :: thesis: verum

end;

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