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 & G is one-to-one ) and
A2: 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:3;
( len F, rng F are_equipotent & len G, rng G are_equipotent ) by A1, WELLORD2:def 4;
then ( card (len F) = card (rng F) & card (len G) = card (rng G) ) by CARD_1:21;
then ( len F = card (rng F) & len G = card (rng G) & card ((rng F) \/ (rng G)) = (card (rng F)) + (card (rng G)) ) by A2, CARD_2:53;
then ( dom (F ^ G) = (len F) + (len G) & (len F) + (len G) = card (rng (F ^ G)) ) by AFINSQ_1:29, AFINSQ_1:def 4;
then ( card (dom (F ^ G)) = card (rng (F ^ G)) & FG is onto ) by FUNCT_2:def 3;
hence F ^ G is one-to-one by STIRL2_1:70; :: thesis: verum