let F, G be XFinSequence; :: thesis: ( F ^ G is one-to-one implies rng F misses rng G )
assume A1: F ^ G is one-to-one ; :: thesis: rng F misses rng G
assume rng F meets rng G ; :: thesis: contradiction
then consider y being object such that
A2: ( y in rng F & y in rng G ) by XBOOLE_0:3;
consider n1 being object such that
A3: ( n1 in dom F & F . n1 = y ) by A2, FUNCT_1:def 3;
consider n2 being object such that
A4: ( n2 in dom G & G . n2 = y ) by A2, FUNCT_1:def 3;
reconsider n1 = n1, n2 = n2 as Nat by A3, A4;
A5: ( (F ^ G) . n1 = F . n1 & (F ^ G) . ((len F) + n2) = G . n2 ) by A3, A4, AFINSQ_1:def 3;
dom F c= dom (F ^ G) by AFINSQ_1:21;
then ( n1 in dom (F ^ G) & (len F) + n2 in dom (F ^ G) ) by A3, A4, AFINSQ_1:23;
then ( n1 = n2 + (len F) & n1 < len F ) by A5, A1, FUNCT_1:def 4, A3, A4, AFINSQ_1:86;
hence contradiction by NAT_1:11; :: thesis: verum