deffunc H1( set ) -> set = \$1;
defpred S1[ set ] means ex r being FinSequence st
( r c= p & r c= q & len r = \$1 );
set S = { H1(k) where k is Nat : ( k <= len p & S1[k] ) } ;
A1: for x being object st x in { H1(k) where k is Nat : ( k <= len p & S1[k] ) } holds
x is natural
proof
let x be object ; :: thesis: ( x in { H1(k) where k is Nat : ( k <= len p & S1[k] ) } implies x is natural )
assume x in { H1(k) where k is Nat : ( k <= len p & S1[k] ) } ; :: thesis: x is natural
then ex n being Nat st
( x = n & n <= len p & S1[n] ) ;
hence x is natural ; :: thesis: verum
end;
A2: { H1(k) where k is Nat : ( k <= len p & S1[k] ) } is finite from ( {} c= p & {} c= q & len {} = 0 ) ;
then 0 in { H1(k) where k is Nat : ( k <= len p & S1[k] ) } ;
then reconsider S = { H1(k) where k is Nat : ( k <= len p & S1[k] ) } as non empty finite natural-membered set by ;
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: S1[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:
dom r c= dom p by ;
then len r <= len p by FINSEQ_3:30;
then len r in S by A8, A9;
then len r <= len R by ;
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
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
.= R . x by ;
:: thesis: verum
end;
hence r is_a_prefix_of R by ; :: thesis: verum