deffunc H_{1}( set ) -> set = $1;

defpred S_{1}[ set ] means ex r being FinSequence st

( r c= p & r c= q & len r = $1 );

set S = { H_{1}(k) where k is Nat : ( k <= len p & S_{1}[k] ) } ;

A1: for x being object st x in { H_{1}(k) where k is Nat : ( k <= len p & S_{1}[k] ) } holds

x is natural_{1}(k) where k is Nat : ( k <= len p & S_{1}[k] ) } is finite
from FINSEQ_1:sch 6();

( {} c= p & {} c= q & len {} = 0 ) ;

then 0 in { H_{1}(k) where k is Nat : ( k <= len p & S_{1}[k] ) }
;

then reconsider S = { H_{1}(k) where k is Nat : ( k <= len p & S_{1}[k] ) } as non empty finite natural-membered set by A1, A2, MEMBERED:def 6;

set maxk = max S;

max S in S by XXREAL_2:def 8;

then consider K being Nat such that

A3: K = max S and

K <= len p and

A4: S_{1}[K]
;

consider R being FinSequence such that

A5: R c= p and

A6: R c= q and

A7: len R = K by A4;

take R ; :: thesis: ( R is_a_prefix_of p & R is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of R ) )

thus R c= p by A5; :: thesis: ( R is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of R ) )

thus R c= q by A6; :: thesis: for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of R

let r be FinSequence; :: thesis: ( r is_a_prefix_of p & r is_a_prefix_of q implies r is_a_prefix_of R )

assume that

A8: r c= p and

A9: r c= q ; :: thesis: r is_a_prefix_of R

dom r c= dom p by A8, GRFUNC_1:2;

then len r <= len p by FINSEQ_3:30;

then len r in S by A8, A9;

then len r <= len R by A3, A7, XXREAL_2:def 8;

then A10: dom r c= dom R by FINSEQ_3:30;

defpred S

( r c= p & r c= q & len r = $1 );

set S = { H

A1: for x being object st x in { H

x is natural

proof

A2:
{ H
let x be object ; :: thesis: ( x in { H_{1}(k) where k is Nat : ( k <= len p & S_{1}[k] ) } implies x is natural )

assume x in { H_{1}(k) where k is Nat : ( k <= len p & S_{1}[k] ) }
; :: thesis: x is natural

then ex n being Nat st

( x = n & n <= len p & S_{1}[n] )
;

hence x is natural ; :: thesis: verum

end;assume x in { H

then ex n being Nat st

( x = n & n <= len p & S

hence x is natural ; :: thesis: verum

( {} c= p & {} c= q & len {} = 0 ) ;

then 0 in { H

then reconsider S = { H

set maxk = max S;

max S in S by XXREAL_2:def 8;

then consider K being Nat such that

A3: K = max S and

K <= len p and

A4: S

consider R being FinSequence such that

A5: R c= p and

A6: R c= q and

A7: len R = K by A4;

take R ; :: thesis: ( R is_a_prefix_of p & R is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of R ) )

thus R c= p by A5; :: thesis: ( R is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of R ) )

thus R c= q by A6; :: thesis: for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds

r is_a_prefix_of R

let r be FinSequence; :: thesis: ( r is_a_prefix_of p & r is_a_prefix_of q implies r is_a_prefix_of R )

assume that

A8: r c= p and

A9: r c= q ; :: thesis: r is_a_prefix_of R

dom r c= dom p by A8, GRFUNC_1:2;

then len r <= len p by FINSEQ_3:30;

then len r in S by A8, A9;

then len r <= len R by A3, A7, XXREAL_2:def 8;

then A10: dom r c= dom R by FINSEQ_3:30;

now :: thesis: for x being object st x in dom r holds

r . x = R . x

hence
r is_a_prefix_of R
by A10, GRFUNC_1:2; :: thesis: verumr . x = R . x

let x be object ; :: thesis: ( x in dom r implies r . x = R . x )

assume A11: x in dom r ; :: thesis: r . x = R . x

hence r . x = p . x by A8, GRFUNC_1:2

.= R . x by A5, A10, A11, GRFUNC_1:2 ;

:: thesis: verum

end;assume A11: x in dom r ; :: thesis: r . x = R . x

hence r . x = p . x by A8, GRFUNC_1:2

.= R . x by A5, A10, A11, GRFUNC_1:2 ;

:: thesis: verum