let F, G be one-to-one FinSequence; :: thesis: ( rng F misses rng G implies F ^ G is one-to-one )
assume A1: rng F misses rng G ; :: thesis: F ^ G is one-to-one
reconsider FG = F ^ G as Function of (dom (F ^ G)),(rng (F ^ G)) by FUNCT_2:1;
A2: FG is onto by FUNCT_2:def 3;
card (dom (F ^ G)) = card (Seg ((len F) + (len G))) by FINSEQ_1:def 7
.= (len F) + (len G) by FINSEQ_1:57
.= (card (rng F)) + (len G) by FINSEQ_4:62
.= (card (rng F)) + (card (rng G)) by FINSEQ_4:62
.= card ((rng F) \/ (rng G)) by A1, CARD_2:40
.= card (rng (F ^ G)) by FINSEQ_1:31 ;
hence F ^ G is one-to-one by A2, FINSEQ_4:63; :: thesis: verum