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 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom (p ^ q) or not b₁ in dom (p ^ q) or not (p ^ q) . x = (p ^ q) . b₁ or x = b₁ )
let y be set ; :: 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

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:38;

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

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

end;

suppose A8: ( 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
A9: n in dom q and
A10: k2 = (len p) + n ;
( (p ^ q) . k1 = p . k1 & (p ^ q) . k2 = q . n ) by A8, A10, FINSEQ_1:def 7;
then ( q . n in rng p & q . n in rng q ) by A6, A8, A9, FUNCT_1:def 5;
hence x = y by A1, XBOOLE_0:3; :: thesis: verum

end;

suppose A11: ( 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
A12: n in dom q and
A13: k1 = (len p) + n ;
( (p ^ q) . k2 = p . k2 & (p ^ q) . k1 = q . n ) by A11, A13, FINSEQ_1:def 7;
then ( q . n in rng p & q . n in rng q ) by A6, A11, A12, FUNCT_1:def 5;
hence x = y by A1, XBOOLE_0:3; :: thesis: verum

end;

suppose A14: ( 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 n1 being Nat such that
A15: n1 in dom q and
A16: k1 = (len p) + n1 ;
consider n2 being Nat such that
A17: n2 in dom q and
A18: k2 = (len p) + n2 by A14;
( (p ^ q) . k1 = q . n1 & (p ^ q) . k2 = q . n2 ) by A15, A16, A17, A18, FINSEQ_1:def 7;
hence x = y by A3, A6, A15, A16, A17, A18, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence x = y ; :: thesis: verum

end;

assume A19: 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 set such that
A20: x in rng p and
A21: x in rng q by XBOOLE_0:3;
consider y1 being set such that
A22: y1 in dom p and
A23: p . y1 = x by A20, FUNCT_1:def 5;
consider y2 being set such that
A24: y2 in dom q and
A25: q . y2 = x by A21, FUNCT_1:def 5;
A26: ( y1 in Seg (len p) & y2 in Seg (len q) ) by A22, A24, FINSEQ_1:def 3;
reconsider y1 = y1, y2 = y2 as Element of NAT by A22, A24;
A27: (len p) + y2 in dom (p ^ q) by A24, FINSEQ_1:41;
( (p ^ q) . y1 = p . y1 & (p ^ q) . ((len p) + y2) = q . y2 & y1 in dom (p ^ q) ) by A22, A24, Th24, FINSEQ_1:def 7;
then A28: y1 = (len p) + y2 by A19, A23, A25, A27, FUNCT_1:def 8;
( y1 <= len p & len p <= (len p) + y2 ) by A26, FINSEQ_1:3, NAT_1:12;
then ( y1 = len p & y1 = y1 + 0 ) by A28, XXREAL_0:1;
hence contradiction by A26, A28, FINSEQ_1:3; :: thesis: verum

end;

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

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom p or not b₁ in dom p or not p . x = p . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom p or not y in dom p or not p . x = p . y or x = y )
assume that
A29: ( x in dom p & y in dom p ) and
A30: p . x = p . y ; :: thesis: x = y
reconsider k = x, l = y as Element of NAT by A29;
( (p ^ q) . k = p . k & (p ^ q) . l = p . l & k in dom (p ^ q) & l in dom (p ^ q) ) by A29, Th24, FINSEQ_1:def 7;
hence x = y by A19, A30, FUNCT_1:def 8; :: thesis: verum

end;

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom q or not b₁ in dom q or not q . x = q . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom q or not y in dom q or not q . x = q . y or x = y )
assume that
A31: x in dom q and
A32: y in dom q and
A33: q . x = q . y ; :: thesis: x = y
consider k being Nat such that
A34: x = k and
A35: (len p) + k in dom (p ^ q) by A31, FINSEQ_1:40;
consider l being Nat such that
A36: y = l and
A37: (len p) + l in dom (p ^ q) by A32, FINSEQ_1:40;
( (p ^ q) . ((len p) + k) = q . k & (p ^ q) . ((len p) + l) = q . l ) by A31, A32, A34, A36, FINSEQ_1:def 7;
then (len p) + k = (len p) + l by A19, A33, A34, A35, A36, A37, FUNCT_1:def 8;
hence x = y by A34, A36; :: thesis: verum