let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f is one-to-one & g is one-to-one & (rng f) /\ (rng g) c= {(g /. 1)} implies f ^' g is one-to-one )
assume that
A1: f is one-to-one and
A2: g is one-to-one and
A3: (rng f) /\ (rng g) c= {(g /. 1)} ; :: thesis: f ^' g is one-to-one
per cases ( rng g <> {} or rng g = {} ) ;
suppose A4: rng g <> {} ; :: thesis: f ^' g is one-to-one
now :: thesis: for i, j being Element of NAT st i in dom (f ^' g) & j in dom (f ^' g) & (f ^' g) /. i = (f ^' g) /. j holds
i = j
A5: (len (f ^' g)) + 1 = (len f) + (len g) by A4, FINSEQ_6:139, RELAT_1:38;
let i, j be Element of NAT ; :: thesis: ( i in dom (f ^' g) & j in dom (f ^' g) & (f ^' g) /. i = (f ^' g) /. j implies i = j )
assume that
A6: i in dom (f ^' g) and
A7: j in dom (f ^' g) and
A8: (f ^' g) /. i = (f ^' g) /. j ; :: thesis: i = j
A9: 1 <= i by A6, FINSEQ_3:25;
j <= len (f ^' g) by A7, FINSEQ_3:25;
then A10: j < (len f) + (len g) by A5, NAT_1:13;
A11: len f = (len f) + 0 ;
i <= len (f ^' g) by A6, FINSEQ_3:25;
then A12: i < (len f) + (len g) by A5, NAT_1:13;
A13: 1 <= j by A7, FINSEQ_3:25;
A14: 1 in dom g by A4, FINSEQ_3:32;
now :: thesis: i = j
per cases ( ( i <= len f & j <= len f ) or ( i > len f & j > len f ) or ( i <= len f & j > len f ) or ( j <= len f & i > len f ) ) ;
suppose A19: ( i > len f & j > len f ) ; :: thesis: i = j
then consider l being Nat such that
A20: j = (len f) + l by NAT_1:10;
consider k being Nat such that
A21: i = (len f) + k by A19, NAT_1:10;
reconsider k = k, l = l as Element of NAT by ORDINAL1:def 12;
l > 0 by A11, A19, A20;
then A22: l >= 0 + 1 by NAT_1:13;
then A23: l + 1 > 1 by NAT_1:13;
k > 0 by A11, A19, A21;
then A24: k >= 0 + 1 by NAT_1:13;
then A25: k + 1 > 1 by NAT_1:13;
A26: l < len g by A10, A20, XREAL_1:7;
then A27: (f ^' g) /. j = g /. (l + 1) by A20, A22, FINSEQ_6:160;
A28: k < len g by A12, A21, XREAL_1:7;
then k + 1 <= len g by NAT_1:13;
then A29: k + 1 in dom g by A25, FINSEQ_3:25;
l + 1 <= len g by A26, NAT_1:13;
then A30: l + 1 in dom g by A23, FINSEQ_3:25;
(f ^' g) /. i = g /. (k + 1) by A21, A28, A24, FINSEQ_6:160;
then k + 1 = l + 1 by A2, A8, A27, A29, A30, PARTFUN2:10;
hence i = j by A21, A20; :: thesis: verum
end;
suppose A31: ( i <= len f & j > len f ) ; :: thesis: i = j
then A32: i in dom f by A9, FINSEQ_3:25;
(f ^' g) /. i = f /. i by A9, A31, FINSEQ_6:159;
then A33: (f ^' g) /. i in rng f by A32, PARTFUN2:2;
consider l being Nat such that
A34: j = (len f) + l by A31, NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
l > 0 by A11, A31, A34;
then A35: l >= 0 + 1 by NAT_1:13;
then A36: l + 1 > 1 by NAT_1:13;
A37: l < len g by A10, A34, XREAL_1:7;
then l + 1 <= len g by NAT_1:13;
then A38: l + 1 in dom g by A36, FINSEQ_3:25;
A39: (f ^' g) /. j = g /. (l + 1) by A34, A37, A35, FINSEQ_6:160;
then (f ^' g) /. j in rng g by A38, PARTFUN2:2;
then (f ^' g) /. j in (rng f) /\ (rng g) by A8, A33, XBOOLE_0:def 4;
then g /. (l + 1) = g /. 1 by A3, A39, TARSKI:def 1;
hence i = j by A2, A14, A36, A38, PARTFUN2:10; :: thesis: verum
end;
suppose A40: ( j <= len f & i > len f ) ; :: thesis: i = j
then A41: j in dom f by A13, FINSEQ_3:25;
(f ^' g) /. j = f /. j by A13, A40, FINSEQ_6:159;
then A42: (f ^' g) /. j in rng f by A41, PARTFUN2:2;
consider l being Nat such that
A43: i = (len f) + l by A40, NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
l > 0 by A11, A40, A43;
then A44: l >= 0 + 1 by NAT_1:13;
then A45: l + 1 > 1 by NAT_1:13;
A46: l < len g by A12, A43, XREAL_1:7;
then l + 1 <= len g by NAT_1:13;
then A47: l + 1 in dom g by A45, FINSEQ_3:25;
A48: (f ^' g) /. i = g /. (l + 1) by A43, A46, A44, FINSEQ_6:160;
then (f ^' g) /. i in rng g by A47, PARTFUN2:2;
then (f ^' g) /. i in (rng f) /\ (rng g) by A8, A42, XBOOLE_0:def 4;
then g /. (l + 1) = g /. 1 by A3, A48, TARSKI:def 1;
hence i = j by A2, A14, A45, A47, PARTFUN2:10; :: thesis: verum
end;
end;
end;
hence i = j ; :: thesis: verum
end;
hence f ^' g is one-to-one by PARTFUN2:9; :: thesis: verum
end;
suppose rng g = {} ; :: thesis: f ^' g is one-to-one
then g = {} by RELAT_1:41;
hence f ^' g is one-to-one by A1, FINSEQ_6:157; :: thesis: verum
end;
end;