let p, q be FinSequence; :: thesis:
let x be object ; :: thesis:
set r = q ^ <*x*>;
set i = (len q) + 1;
assume that
A1: q ^ <*x*> is one-to-one and
A2: rng (q ^ <*x*>) c= rng p ; :: thesis:
A3: (q ^ <*x*>) . ((len q) + 1) = x by FINSEQ_1:42;
rng q c= rng (q ^ <*x*>) by FINSEQ_1:29;
then A4: rng q c= rng p by A2;
( len (q ^ <*x*>) = (len q) + 1 & 1 <= (len q) + 1 ) by FINSEQ_2:16, NAT_1:11;
then A5: (len q) + 1 in dom (q ^ <*x*>) by FINSEQ_3:25;
then consider y being object such that
A6: y in dom p and
A7: (q ^ <*x*>) . ((len q) + 1) = p . y by A2, FUNCT_1:114;
reconsider j = y as Element of NAT by A6;
j <= len p by A6, FINSEQ_3:25;
then consider k being Nat such that
A8: len p = j + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
consider s, p2 being FinSequence such that
A9: len s = j and
len p2 = k and
A10: p = s ^ p2 by A8, FINSEQ_2:22;
A11: 1 <= j by A6, FINSEQ_3:25;
then ex m being Nat st j = 1 + m by NAT_1:10;
then consider p1 being FinSequence, d being object such that
A12: s = p1 ^ <*d*> by A9, FINSEQ_2:18;
j in dom s by A9, A11, FINSEQ_3:25;
then A13: s . j = x by A7, A10, A3, FINSEQ_1:def 7;
take p1 ; :: thesis:
take p2 ; :: thesis:
A14: j = (len p1) + 1 by A9, A12, FINSEQ_2:16;
hence p = (p1 ^ <*x*>) ^ p2 by A10, A12, A13, FINSEQ_1:42; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: y in rng q ; :: thesis:

end;