let p be FinSequence; :: thesis: for x being set st x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) holds
p is one-to-one
let x be set ; :: thesis: ( x in rng p & p - {x} is one-to-one & p - {x} = (p -| x) ^ (p |-- x) implies p is one-to-one )
assume that
A1: x in rng p and
A2: p - {x} is one-to-one and
A3: p - {x} = (p -| x) ^ (p |-- x) ; :: thesis: p is one-to-one
let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x1 in dom p or not b₁ in dom p or not p . x1 = p . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in dom p or not x2 in dom p or not p . x1 = p . x2 or x1 = x2 )
set q = p - {x};
assume that
A4: x1 in dom p and
A5: x2 in dom p and
A6: p . x1 = p . x2 ; :: thesis: x1 = x2
reconsider k1 = x1, k2 = x2 as Element of NAT by A4, A5;
A7: p just_once_values x by A1, A3, Th69;

now

per cases ( ( x1 = x .. p & x2 = x .. p ) or ( x1 = x .. p & x .. p < k2 ) or ( x1 = x .. p & k2 < x .. p ) or ( k1 < x .. p & x .. p = x2 ) or ( k1 < x .. p & x .. p < k2 ) or ( k1 < x .. p & k2 < x .. p ) or ( x .. p < k1 & x .. p < k2 ) or ( x .. p < k1 & x .. p = x2 ) or ( x .. p < k1 & k2 < x .. p ) ) by XXREAL_0:1;

suppose ( x1 = x .. p & x2 = x .. p ) ; :: thesis: x1 = x2

hence x1 = x2 ; :: thesis: verum

end;

suppose ( x1 = x .. p & x .. p < k2 ) ; :: thesis: x1 = x2

hence x1 = x2 by A1, A5, A6, A7, Th29, Th36; :: thesis: verum

end;

suppose ( x1 = x .. p & k2 < x .. p ) ; :: thesis: x1 = x2

hence x1 = x2 by A1, A5, A6, A7, Th29, Th36; :: thesis: verum

end;

suppose ( k1 < x .. p & x .. p = x2 ) ; :: thesis: x1 = x2

hence x1 = x2 by A1, A4, A6, A7, Th29, Th36; :: thesis: verum

end;

suppose A8: ( k1 < x .. p & x .. p < k2 ) ; :: thesis: x1 = x2

then k2 <> 0 by NAT_1:2;
then consider m2 being Nat such that
A9: k2 = m2 + 1 by NAT_1:6;
reconsider m2 = m2 as Element of NAT by ORDINAL1:def 13;
k1 in Seg (len p) by A4, FINSEQ_1:def 3;
then A10: 1 <= k1 by FINSEQ_1:3;
x .. p <= len p by A1, Th31;
then k1 < len p by A8, XXREAL_0:2;
then k1 + 1 <= len p by NAT_1:13;
then k1 <= (len p) - 1 by XREAL_1:21;
then k1 <= len (p - {x}) by A7, Th40;
then k1 in Seg (len (p - {x})) by A10;
then A11: k1 in dom (p - {x}) by FINSEQ_1:def 3;
A12: x .. p <= m2 by A8, A9, NAT_1:13;
1 <= x .. p by A1, Th31;
then A13: 1 <= m2 by A12, XXREAL_0:2;
k2 in Seg (len p) by A5, FINSEQ_1:def 3;
then k2 <= len p by FINSEQ_1:3;
then m2 <= (len p) - 1 by A9, XREAL_1:21;
then m2 <= len (p - {x}) by A7, Th40;
then m2 in Seg (len (p - {x})) by A13;
then A14: m2 in dom (p - {x}) by FINSEQ_1:def 3;
then ( (p - {x}) . k1 = p . k1 & (p - {x}) . m2 = p . k2 ) by A7, A8, A9, A11, A12, Th41;
hence x1 = x2 by A2, A6, A8, A11, A12, A14, FUNCT_1:def 8; :: thesis: verum

end;

suppose A15: ( k1 < x .. p & k2 < x .. p ) ; :: thesis: x1 = x2

( k1 in Seg (len p) & k2 in Seg (len p) ) by A4, A5, FINSEQ_1:def 3;
then A16: ( 1 <= k1 & 1 <= k2 ) by FINSEQ_1:3;
x .. p <= len p by A1, Th31;
then ( k1 < len p & k2 < len p ) by A15, XXREAL_0:2;
then ( k1 + 1 <= len p & k2 + 1 <= len p ) by NAT_1:13;
then ( k1 <= (len p) - 1 & k2 <= (len p) - 1 ) by XREAL_1:21;
then ( k1 <= len (p - {x}) & k2 <= len (p - {x}) ) by A7, Th40;
then ( k1 in Seg (len (p - {x})) & k2 in Seg (len (p - {x})) ) by A16;
then A17: ( k1 in dom (p - {x}) & k2 in dom (p - {x}) ) by FINSEQ_1:def 3;
then ( p . k1 = (p - {x}) . k1 & p . k2 = (p - {x}) . k2 ) by A7, A15, Th41;
hence x1 = x2 by A2, A6, A17, FUNCT_1:def 8; :: thesis: verum

end;

suppose A18: ( x .. p < k1 & x .. p < k2 ) ; :: thesis: x1 = x2

then A19: ( k1 <> 0 & k2 <> 0 ) by NAT_1:2;
then consider m1 being Nat such that
A20: k1 = m1 + 1 by NAT_1:6;
consider m2 being Nat such that
A21: k2 = m2 + 1 by A19, NAT_1:6;
reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def 13;
A22: ( x .. p <= m1 & x .. p <= m2 ) by A18, A20, A21, NAT_1:13;
1 <= x .. p by A1, Th31;
then A23: ( 1 <= m1 & 1 <= m2 ) by A22, XXREAL_0:2;
( k1 in Seg (len p) & k2 in Seg (len p) ) by A4, A5, FINSEQ_1:def 3;
then ( k1 <= len p & k2 <= len p ) by FINSEQ_1:3;
then ( m1 <= (len p) - 1 & m2 <= (len p) - 1 ) by A20, A21, XREAL_1:21;
then ( m1 <= len (p - {x}) & m2 <= len (p - {x}) ) by A7, Th40;
then ( m1 in Seg (len (p - {x})) & m2 in Seg (len (p - {x})) ) by A23;
then A24: ( m1 in dom (p - {x}) & m2 in dom (p - {x}) ) by FINSEQ_1:def 3;
then ( p . k1 = (p - {x}) . m1 & p . k2 = (p - {x}) . m2 ) by A7, A20, A21, A22, Th41;
hence x1 = x2 by A2, A6, A20, A21, A24, FUNCT_1:def 8; :: thesis: verum

end;

suppose ( x .. p < k1 & x .. p = x2 ) ; :: thesis: x1 = x2

hence x1 = x2 by A1, A4, A6, A7, Th29, Th36; :: thesis: verum

end;

suppose A25: ( x .. p < k1 & k2 < x .. p ) ; :: thesis: x1 = x2

then k1 <> 0 by NAT_1:2;
then consider m2 being Nat such that
A26: k1 = m2 + 1 by NAT_1:6;
reconsider m2 = m2 as Element of NAT by ORDINAL1:def 13;
k2 in Seg (len p) by A5, FINSEQ_1:def 3;
then A27: 1 <= k2 by FINSEQ_1:3;
x .. p <= len p by A1, Th31;
then k2 < len p by A25, XXREAL_0:2;
then k2 + 1 <= len p by NAT_1:13;
then k2 <= (len p) - 1 by XREAL_1:21;
then k2 <= len (p - {x}) by A7, Th40;
then k2 in Seg (len (p - {x})) by A27;
then A28: k2 in dom (p - {x}) by FINSEQ_1:def 3;
A29: x .. p <= m2 by A25, A26, NAT_1:13;
1 <= x .. p by A1, Th31;
then A30: 1 <= m2 by A29, XXREAL_0:2;
k1 in Seg (len p) by A4, FINSEQ_1:def 3;
then k1 <= len p by FINSEQ_1:3;
then m2 <= (len p) - 1 by A26, XREAL_1:21;
then m2 <= len (p - {x}) by A7, Th40;
then m2 in Seg (len (p - {x})) by A30;
then A31: m2 in dom (p - {x}) by FINSEQ_1:def 3;
then ( (p - {x}) . k2 = p . k2 & (p - {x}) . m2 = p . k1 ) by A7, A25, A26, A28, A29, Th41;
hence x1 = x2 by A2, A6, A25, A28, A29, A31, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum