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 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 A5:
i in dom (f ^' g)
and A6:
j in dom (f ^' g)
and A7:
(f ^' g) /. i = (f ^' g) /. j
;
:: thesis: i = jA8:
( 1
<= i &
i <= len (f ^' g) )
by A5, FINSEQ_3:27;
A9:
( 1
<= j &
j <= len (f ^' g) )
by A6, FINSEQ_3:27;
g <> {}
by A4, RELAT_1:60;
then
(len (f ^' g)) + 1
= (len f) + (len g)
by GRAPH_2:13;
then A10:
(
i < (len f) + (len g) &
j < (len f) + (len g) )
by A8, A9, NAT_1:13;
A11:
len f = (len f) + 0
;
A12:
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 )
;
:: thesis: i = jthen consider k being
Nat such that A16:
i = (len f) + k
by NAT_1:10;
consider l being
Nat such that A17:
j = (len f) + l
by A15, NAT_1:10;
reconsider k =
k,
l =
l as
Element of
NAT by ORDINAL1:def 13;
A18:
(
k < len g &
l < len g )
by A10, A16, A17, XREAL_1:9;
k > 0
by A11, A15, A16;
then A19:
k >= 0 + 1
by NAT_1:13;
then A20:
(f ^' g) /. i = g /. (k + 1)
by A16, A18, GRAPH_2:62;
l > 0
by A11, A15, A17;
then A21:
l >= 0 + 1
by NAT_1:13;
then A22:
(f ^' g) /. j = g /. (l + 1)
by A17, A18, GRAPH_2:62;
A23:
(
k + 1
<= len g &
l + 1
<= len g )
by A18, NAT_1:13;
(
k + 1
> 1 &
l + 1
> 1 )
by A19, A21, NAT_1:13;
then
(
k + 1
in dom g &
l + 1
in dom g )
by A23, FINSEQ_3:27;
then
k + 1
= l + 1
by A2, A7, A20, A22, PARTFUN2:17;
hence
i = j
by A16, A17;
:: thesis: verum end; suppose A24:
(
i <= len f &
j > len f )
;
:: thesis: i = jthen A25:
(f ^' g) /. i = f /. i
by A8, GRAPH_2:61;
i in dom f
by A8, A24, FINSEQ_3:27;
then A26:
(f ^' g) /. i in rng f
by A25, PARTFUN2:4;
consider l being
Nat such that A27:
j = (len f) + l
by A24, NAT_1:10;
reconsider l =
l as
Element of
NAT by ORDINAL1:def 13;
A28:
l < len g
by A10, A27, XREAL_1:9;
l > 0
by A11, A24, A27;
then A29:
l >= 0 + 1
by NAT_1:13;
then A30:
(f ^' g) /. j = g /. (l + 1)
by A27, A28, GRAPH_2:62;
A31:
l + 1
<= len g
by A28, NAT_1:13;
A32:
l + 1
> 1
by A29, NAT_1:13;
then A33:
l + 1
in dom g
by A31, FINSEQ_3:27;
then
(f ^' g) /. j in rng g
by A30, PARTFUN2:4;
then
(f ^' g) /. j in (rng f) /\ (rng g)
by A7, A26, XBOOLE_0:def 4;
then
g /. (l + 1) = g /. 1
by A3, A30, TARSKI:def 1;
hence
i = j
by A2, A12, A32, A33, PARTFUN2:17;
:: thesis: verum end; suppose A34:
(
j <= len f &
i > len f )
;
:: thesis: i = jthen A35:
(f ^' g) /. j = f /. j
by A9, GRAPH_2:61;
j in dom f
by A9, A34, FINSEQ_3:27;
then A36:
(f ^' g) /. j in rng f
by A35, PARTFUN2:4;
consider l being
Nat such that A37:
i = (len f) + l
by A34, NAT_1:10;
reconsider l =
l as
Element of
NAT by ORDINAL1:def 13;
A38:
l < len g
by A10, A37, XREAL_1:9;
l > 0
by A11, A34, A37;
then A39:
l >= 0 + 1
by NAT_1:13;
then A40:
(f ^' g) /. i = g /. (l + 1)
by A37, A38, GRAPH_2:62;
A41:
l + 1
<= len g
by A38, NAT_1:13;
A42:
l + 1
> 1
by A39, NAT_1:13;
then A43:
l + 1
in dom g
by A41, FINSEQ_3:27;
then
(f ^' g) /. i in rng g
by A40, PARTFUN2:4;
then
(f ^' g) /. i in (rng f) /\ (rng g)
by A7, A36, XBOOLE_0:def 4;
then
g /. (l + 1) = g /. 1
by A3, A40, TARSKI:def 1;
hence
i = j
by A2, A12, A42, A43, PARTFUN2:17;
:: thesis: verum end; hence
i = j
;
:: thesis: verum end; hence
f ^' g is
one-to-one
by PARTFUN2:16;
:: thesis: verum