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:64; :: thesis: verum

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:64; :: thesis: verum