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
set q = p - {x};
let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b1 being set holds
( not x1 in proj1 p or not b1 in proj1 p or not p . x1 = p . b1 or x1 = b1 )
let x2 be set ; :: thesis: ( not x1 in proj1 p or not x2 in proj1 p or not p . x1 = p . x2 or x1 = x2 )
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
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 A9: k1 <= len (p - {x}) by A7, Th40;
k1 in Seg (len p) by A4, FINSEQ_1:def 3;
then 1 <= k1 by FINSEQ_1:3;
then k1 in Seg (len (p - {x})) by A9;
then A10: k1 in dom (p - {x}) by FINSEQ_1:def 3;
then A11: (p - {x}) . k1 = p . k1 by A7, A8, Th41;
k2 <> 0 by A8, NAT_1:2;
then consider m2 being Nat such that
A12: k2 = m2 + 1 by NAT_1:6;
reconsider m2 = m2 as Element of NAT by ORDINAL1:def 13;
A13: x .. p <= m2 by A8, A12, NAT_1:13;
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 A12, XREAL_1:21;
then A14: m2 <= len (p - {x}) by A7, Th40;
1 <= x .. p by A1, Th31;
then 1 <= m2 by A13, XXREAL_0:2;
then m2 in Seg (len (p - {x})) by A14;
then A15: m2 in dom (p - {x}) by FINSEQ_1:def 3;
then (p - {x}) . m2 = p . k2 by A7, A12, A13, Th41;
hence x1 = x2 by A2, A6, A8, A10, A13, A15, A11, FUNCT_1:def 8; :: thesis: verum
end;
suppose A16: ( k1 < x .. p & k2 < x .. p ) ; :: thesis: x1 = x2
A17: x .. p <= len p by A1, Th31;
then k2 < len p by A16, XXREAL_0:2;
then k2 + 1 <= len p by NAT_1:13;
then k2 <= (len p) - 1 by XREAL_1:21;
then A18: k2 <= len (p - {x}) by A7, Th40;
k2 in Seg (len p) by A5, FINSEQ_1:def 3;
then 1 <= k2 by FINSEQ_1:3;
then k2 in Seg (len (p - {x})) by A18;
then A19: k2 in dom (p - {x}) by FINSEQ_1:def 3;
then A20: p . k2 = (p - {x}) . k2 by A7, A16, Th41;
k1 < len p by A16, A17, XXREAL_0:2;
then k1 + 1 <= len p by NAT_1:13;
then k1 <= (len p) - 1 by XREAL_1:21;
then A21: k1 <= len (p - {x}) by A7, Th40;
k1 in Seg (len p) by A4, FINSEQ_1:def 3;
then 1 <= k1 by FINSEQ_1:3;
then k1 in Seg (len (p - {x})) by A21;
then A22: k1 in dom (p - {x}) by FINSEQ_1:def 3;
then p . k1 = (p - {x}) . k1 by A7, A16, Th41;
hence x1 = x2 by A2, A6, A22, A19, A20, FUNCT_1:def 8; :: thesis: verum
end;
suppose A23: ( x .. p < k1 & x .. p < k2 ) ; :: thesis: x1 = x2
then k2 <> 0 by NAT_1:2;
then consider m2 being Nat such that
A24: k2 = m2 + 1 by NAT_1:6;
k1 <> 0 by A23, NAT_1:2;
then consider m1 being Nat such that
A25: k1 = m1 + 1 by NAT_1:6;
reconsider m1 = m1, m2 = m2 as Element of NAT by ORDINAL1:def 13;
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 A24, XREAL_1:21;
then A26: m2 <= len (p - {x}) by A7, Th40;
A27: 1 <= x .. p by A1, Th31;
A28: x .. p <= m2 by A23, A24, NAT_1:13;
then 1 <= m2 by A27, XXREAL_0:2;
then m2 in Seg (len (p - {x})) by A26;
then A29: m2 in dom (p - {x}) by FINSEQ_1:def 3;
then A30: p . k2 = (p - {x}) . m2 by A7, A24, A28, Th41;
k1 in Seg (len p) by A4, FINSEQ_1:def 3;
then k1 <= len p by FINSEQ_1:3;
then m1 <= (len p) - 1 by A25, XREAL_1:21;
then A31: m1 <= len (p - {x}) by A7, Th40;
A32: x .. p <= m1 by A23, A25, NAT_1:13;
then 1 <= m1 by A27, XXREAL_0:2;
then m1 in Seg (len (p - {x})) by A31;
then A33: m1 in dom (p - {x}) by FINSEQ_1:def 3;
then p . k1 = (p - {x}) . m1 by A7, A25, A32, Th41;
hence x1 = x2 by A2, A6, A25, A24, A33, A29, A30, 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 A34: ( x .. p < k1 & k2 < x .. p ) ; :: thesis: x1 = x2
x .. p <= len p by A1, Th31;
then k2 < len p by A34, XXREAL_0:2;
then k2 + 1 <= len p by NAT_1:13;
then k2 <= (len p) - 1 by XREAL_1:21;
then A35: k2 <= len (p - {x}) by A7, Th40;
k2 in Seg (len p) by A5, FINSEQ_1:def 3;
then 1 <= k2 by FINSEQ_1:3;
then k2 in Seg (len (p - {x})) by A35;
then A36: k2 in dom (p - {x}) by FINSEQ_1:def 3;
then A37: (p - {x}) . k2 = p . k2 by A7, A34, Th41;
k1 <> 0 by A34, NAT_1:2;
then consider m2 being Nat such that
A38: k1 = m2 + 1 by NAT_1:6;
reconsider m2 = m2 as Element of NAT by ORDINAL1:def 13;
A39: x .. p <= m2 by A34, A38, NAT_1:13;
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 A38, XREAL_1:21;
then A40: m2 <= len (p - {x}) by A7, Th40;
1 <= x .. p by A1, Th31;
then 1 <= m2 by A39, XXREAL_0:2;
then m2 in Seg (len (p - {x})) by A40;
then A41: m2 in dom (p - {x}) by FINSEQ_1:def 3;
then (p - {x}) . m2 = p . k1 by A7, A38, A39, Th41;
hence x1 = x2 by A2, A6, A34, A36, A39, A41, A37, FUNCT_1:def 8; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum