let D be non empty set ; :: thesis: for r being FinSequence of D
for r1, r2 being FinSequence
for k being Nat st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
let r be FinSequence of D; :: thesis: for r1, r2 being FinSequence
for k being Nat st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
let r1, r2 be FinSequence; :: thesis: for k being Nat st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
let k be Nat; :: thesis: ( k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) implies ex x being Element of D st r1 = r2 ^ <*x*> )
assume that
A1: k + 1 <= len r and
A2: r1 = r | (Seg (k + 1)) and
A3: r2 = r | (Seg k) ; :: thesis: ex x being Element of D st r1 = r2 ^ <*x*>
k < len r by A1, NAT_1:13;
then A4: len r2 = k by A3, FINSEQ_1:17;
r2 is_a_prefix_of r by A3, TREES_1:def 1;
then A5: ex q2 being FinSequence st r = r2 ^ q2 by TREES_1:1;
then reconsider r99 = r2 as FinSequence of D by FINSEQ_1:36;
r1 is_a_prefix_of r by A2, TREES_1:def 1;
then A6: ex q1 being FinSequence st r = r1 ^ q1 by TREES_1:1;
then reconsider r9 = r1 as FinSequence of D by FINSEQ_1:36;
A7: len r1 = k + 1 by A1, A2, FINSEQ_1:17;
A8: now :: thesis: not r9 is_a_prefix_of r99
assume r9 is_a_prefix_of r99 ; :: thesis: contradiction
then k + 1 <= k + 0 by A7, A4, NAT_1:43;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
r9,r99 are_c=-comparable by A6, A5, TREES_A:1;
then r99 is_a_prefix_of r9 by A8;
then consider s being FinSequence such that
A9: r9 = r99 ^ s by TREES_1:1;
reconsider s = s as FinSequence of D by A9, FINSEQ_1:36;
A10: len s = 1
proof
consider m being Nat such that
A11: m = len s ;
k + 1 = k + m by A7, A4, A9, A11, FINSEQ_1:22;
hence len s = 1 by A11; :: thesis: verum
end;
consider x being set such that
A12: x = s . 1 ;
1 in {1} by TARSKI:def 1;
then 1 in dom s by A10, FINSEQ_1:2, FINSEQ_1:def 3;
then A13: x in rng s by A12, FUNCT_1:def 3;
s = <*x*> by A10, A12, FINSEQ_1:40;
hence ex x being Element of D st r1 = r2 ^ <*x*> by A9, A13; :: thesis: verum