let n be Nat; for p, r being FinSequence st r = p | (Seg n) holds
ex q being FinSequence st p = r ^ q
let p, r be FinSequence; ( r = p | (Seg n) implies ex q being FinSequence st p = r ^ q )
assume A1:
r = p | (Seg n)
; ex q being FinSequence st p = r ^ q
then consider m being Nat such that
A2:
len p = (len r) + m
by Th79, NAT_1:10;
deffunc H1( Nat) -> set = p . ((len r) + $1);
consider q being FinSequence such that
A3:
( len q = m & ( for k being Nat st k in dom q holds
q . k = H1(k) ) )
from FINSEQ_1:sch 2();
take
q
; p = r ^ q
A4:
len p = len (r ^ q)
by A2, A3, Th22;
now for k being Nat st 1 <= k & k <= len p holds
p . k = (r ^ q) . klet k be
Nat;
( 1 <= k & k <= len p implies p . k = (r ^ q) . k )assume that A5:
1
<= k
and A6:
k <= len p
;
p . k = (r ^ q) . know ( not k <= len r implies p . k = (r ^ q) . k )assume A10:
not
k <= len r
;
p . k = (r ^ q) . kthen consider j being
Nat such that A11:
k = (len r) + j
by NAT_1:10;
k - (len r) = j
by A11;
then A12:
(r ^ q) . k = q . j
by A4, A6, A10, Th24;
j <> 0
by A10, A11;
then A13:
0 + 1
<= j
by NAT_1:13;
j <= len q
by A2, A3, A6, A11, XREAL_1:6;
then
j in Seg m
by A3, A13;
then
j in dom q
by A3, Def3;
hence
p . k = (r ^ q) . k
by A3, A11, A12;
verum end; hence
p . k = (r ^ q) . k
by A7;
verum end;
hence
p = r ^ q
by A4, Th14; verum