let F, G be XFinSequence; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum