let F, G be XFinSequence; ( F is one-to-one & G is one-to-one & rng F misses rng G 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 misses rng G
; F ^ G is one-to-one
len F, rng F are_equipotent
by A1, WELLORD2:def 4;
then A4:
card (len F) = card (rng F)
by CARD_1:5;
len G, rng G are_equipotent
by A2, WELLORD2:def 4;
then A5:
card (len G) = card (rng G)
by CARD_1:5;
reconsider FG = F ^ G as Function of (dom (F ^ G)),(rng (F ^ G)) by FUNCT_2:1;
A6:
dom (F ^ G) = (len F) + (len G)
by AFINSQ_1:def 3;
A7:
FG is onto
by FUNCT_2:def 3;
card ((rng F) \/ (rng G)) = (card (rng F)) + (card (rng G))
by A3, CARD_2:40;
then
card (dom (F ^ G)) = card (rng (F ^ G))
by A4, A5, A6, AFINSQ_1:26;
hence
F ^ G is one-to-one
by A7, FINSEQ_4:63; verum