let p, q be FinSequence; :: thesis: ( ( rng p misses rng q & p is one-to-one & q is one-to-one ) iff p ^ q is one-to-one )
thus ( rng p misses rng q & p is one-to-one & q is one-to-one implies p ^ q is one-to-one ) :: thesis: ( p ^ q is one-to-one implies ( rng p misses rng q & p is one-to-one & q is one-to-one ) )

proof

assume that
A1: rng p misses rng q and
A2: p is one-to-one and
A3: q is one-to-one ; :: thesis: p ^ q is one-to-one
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (p ^ q) or not y in dom (p ^ q) or not (p ^ q) . x = (p ^ q) . y or x = y )
assume that
A4: x in dom (p ^ q) and
A5: y in dom (p ^ q) and
A6: (p ^ q) . x = (p ^ q) . y ; :: thesis: x = y
reconsider k1 = x, k2 = y as Element of NAT by A4, A5;

now :: thesis: x = y

per cases ( ( k1 in dom p & k2 in dom p ) or ( k1 in dom p & ex n being Nat st
( n in dom q & k2 = (len p) + n ) ) or ( k2 in dom p & ex n being Nat st
( n in dom q & k1 = (len p) + n ) ) or ( ex n being Nat st
( n in dom q & k1 = (len p) + n ) & ex n being Nat st
( n in dom q & k2 = (len p) + n ) ) ) by A4, A5, FINSEQ_1:25;

suppose A7: ( k1 in dom p & k2 in dom p ) ; :: thesis: x = y

then A8: (p ^ q) . k2 = p . k2 by FINSEQ_1:def 7;
(p ^ q) . k1 = p . k1 by A7, FINSEQ_1:def 7;
hence x = y by A2, A6, A7, A8; :: thesis: verum

end;

suppose A9: ( k1 in dom p & ex n being Nat st
( n in dom q & k2 = (len p) + n ) ) ; :: thesis: x = y

then consider n being Nat such that
A10: n in dom q and
A11: k2 = (len p) + n ;
A12: q . n in rng q by A10, FUNCT_1:def 3;
A13: (p ^ q) . k1 = p . k1 by A9, FINSEQ_1:def 7;
(p ^ q) . k2 = q . n by A9, A11, FINSEQ_1:def 7;
then q . n in rng p by A6, A9, A13, FUNCT_1:def 3;
hence x = y by A1, A12, XBOOLE_0:3; :: thesis: verum

end;

suppose A14: ( k2 in dom p & ex n being Nat st
( n in dom q & k1 = (len p) + n ) ) ; :: thesis: x = y

then consider n being Nat such that
A15: n in dom q and
A16: k1 = (len p) + n ;
A17: q . n in rng q by A15, FUNCT_1:def 3;
A18: (p ^ q) . k2 = p . k2 by A14, FINSEQ_1:def 7;
(p ^ q) . k1 = q . n by A14, A16, FINSEQ_1:def 7;
then q . n in rng p by A6, A14, A18, FUNCT_1:def 3;
hence x = y by A1, A17, XBOOLE_0:3; :: thesis: verum

end;

suppose A19: ( ex n being Nat st
( n in dom q & k1 = (len p) + n ) & ex n being Nat st
( n in dom q & k2 = (len p) + n ) ) ; :: thesis: x = y

then consider n2 being Nat such that
A20: n2 in dom q and
A21: k2 = (len p) + n2 ;
A22: (p ^ q) . k2 = q . n2 by A20, A21, FINSEQ_1:def 7;
consider n1 being Nat such that
A23: n1 in dom q and
A24: k1 = (len p) + n1 by A19;
(p ^ q) . k1 = q . n1 by A23, A24, FINSEQ_1:def 7;
hence x = y by A3, A6, A23, A24, A20, A21, A22; :: thesis: verum

end;

end;

end;

hence x = y ; :: thesis: verum

end;

assume A25: p ^ q is one-to-one ; :: thesis: ( rng p misses rng q & p is one-to-one & q is one-to-one )
thus rng p misses rng q :: thesis: ( p is one-to-one & q is one-to-one )

proof

assume not rng p misses rng q ; :: thesis: contradiction
then consider x being object such that
A26: x in rng p and
A27: x in rng q by XBOOLE_0:3;
consider y1 being object such that
A28: y1 in dom p and
A29: p . y1 = x by A26, FUNCT_1:def 3;
A30: y1 in Seg (len p) by A28, FINSEQ_1:def 3;
consider y2 being object such that
A31: y2 in dom q and
A32: q . y2 = x by A27, FUNCT_1:def 3;
A33: y2 in Seg (len q) by A31, FINSEQ_1:def 3;
reconsider y1 = y1, y2 = y2 as Element of NAT by A28, A31;
A34: (len p) + y2 in dom (p ^ q) by A31, FINSEQ_1:28;
A35: (p ^ q) . y1 = p . y1 by A28, FINSEQ_1:def 7;
A36: (p ^ q) . ((len p) + y2) = q . y2 by A31, FINSEQ_1:def 7;
y1 in dom (p ^ q) by A28, Th22;
then A37: y1 = (len p) + y2 by A25, A29, A32, A34, A35, A36;
A38: y1 = y1 + 0 ;
A39: len p <= (len p) + y2 by NAT_1:12;
y1 <= len p by A30, FINSEQ_1:1;
then y1 = len p by A37, A39, XXREAL_0:1;
hence contradiction by A33, A37, A38, FINSEQ_1:1; :: thesis: verum

end;

thus p is one-to-one :: thesis: q is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom p or not y in dom p or not p . x = p . y or x = y )
assume that
A40: x in dom p and
A41: y in dom p and
A42: p . x = p . y ; :: thesis: x = y
reconsider k = x, l = y as Element of NAT by A40, A41;
A43: (p ^ q) . k = p . k by A40, FINSEQ_1:def 7;
A44: (p ^ q) . l = p . l by A41, FINSEQ_1:def 7;
A45: l in dom (p ^ q) by A41, Th22;
k in dom (p ^ q) by A40, Th22;
hence x = y by A25, A42, A43, A44, A45; :: thesis: verum

end;

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom q or not y in dom q or not q . x = q . y or x = y )
assume that
A46: x in dom q and
A47: y in dom q and
A48: q . x = q . y ; :: thesis: x = y
consider l being Nat such that
A49: y = l and
A50: (len p) + l in dom (p ^ q) by A47, FINSEQ_1:27;
A51: (p ^ q) . ((len p) + l) = q . l by A47, A49, FINSEQ_1:def 7;
consider k being Nat such that
A52: x = k and
A53: (len p) + k in dom (p ^ q) by A46, FINSEQ_1:27;
(p ^ q) . ((len p) + k) = q . k by A46, A52, FINSEQ_1:def 7;
then (len p) + k = (len p) + l by A25, A48, A52, A53, A49, A50, A51;
hence x = y by A52, A49; :: thesis: verum