let f, g be FinSequence of (TOP-REAL 2); ( 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)}
; f ^' g is one-to-one
per cases
( rng g <> {} or rng g = {} )
;
suppose A4:
rng g <> {}
;
f ^' g is one-to-one now A5:
(len (f ^' g)) + 1
= (len f) + (len g)
by A4, GRAPH_2:13, RELAT_1:60;
let i,
j be
Element of
NAT ;
( 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
;
i = jA9:
1
<= i
by A6, FINSEQ_3:27;
j <= len (f ^' g)
by A7, FINSEQ_3:27;
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:27;
then A12:
i < (len f) + (len g)
by A5, NAT_1:13;
A13:
1
<= j
by A7, FINSEQ_3:27;
A14:
1
in dom g
by A4, FINSEQ_3:34;
now 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 A15:
(
i <= len f &
j <= len f )
;
i = jthen A16:
i in dom f
by A9, FINSEQ_3:27;
A17:
(f ^' g) /. j = f /. j
by A13, A15, GRAPH_2:61;
A18:
j in dom f
by A13, A15, FINSEQ_3:27;
(f ^' g) /. i = f /. i
by A9, A15, GRAPH_2:61;
hence
i = j
by A1, A8, A17, A16, A18, PARTFUN2:17;
verum end; suppose A19:
(
i > len f &
j > len f )
;
i = jthen 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 13;
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:9;
then A27:
(f ^' g) /. j = g /. (l + 1)
by A20, A22, GRAPH_2:62;
A28:
k < len g
by A12, A21, XREAL_1:9;
then
k + 1
<= len g
by NAT_1:13;
then A29:
k + 1
in dom g
by A25, FINSEQ_3:27;
l + 1
<= len g
by A26, NAT_1:13;
then A30:
l + 1
in dom g
by A23, FINSEQ_3:27;
(f ^' g) /. i = g /. (k + 1)
by A21, A28, A24, GRAPH_2:62;
then
k + 1
= l + 1
by A2, A8, A27, A29, A30, PARTFUN2:17;
hence
i = j
by A21, A20;
verum end; suppose A31:
(
i <= len f &
j > len f )
;
i = jthen A32:
i in dom f
by A9, FINSEQ_3:27;
(f ^' g) /. i = f /. i
by A9, A31, GRAPH_2:61;
then A33:
(f ^' g) /. i in rng f
by A32, PARTFUN2:4;
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 13;
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:9;
then
l + 1
<= len g
by NAT_1:13;
then A38:
l + 1
in dom g
by A36, FINSEQ_3:27;
A39:
(f ^' g) /. j = g /. (l + 1)
by A34, A37, A35, GRAPH_2:62;
then
(f ^' g) /. j in rng g
by A38, PARTFUN2:4;
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:17;
verum end; suppose A40:
(
j <= len f &
i > len f )
;
i = jthen A41:
j in dom f
by A13, FINSEQ_3:27;
(f ^' g) /. j = f /. j
by A13, A40, GRAPH_2:61;
then A42:
(f ^' g) /. j in rng f
by A41, PARTFUN2:4;
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 13;
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:9;
then
l + 1
<= len g
by NAT_1:13;
then A47:
l + 1
in dom g
by A45, FINSEQ_3:27;
A48:
(f ^' g) /. i = g /. (l + 1)
by A43, A46, A44, GRAPH_2:62;
then
(f ^' g) /. i in rng g
by A47, PARTFUN2:4;
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:17;
verum end; hence
i = j
;
verum end; hence
f ^' g is
one-to-one
by PARTFUN2:16;
verum