deffunc H₁( set ) -> set = $1;
defpred S₁[ set ] means ex r being FinSequence st
( r c= p & r c= q & len r = $1 );
set S = { H₁(k) where k is Nat : ( k <= len p & S₁[k] ) } ;
A1: for x being object st x in { H₁(k) where k is Nat : ( k <= len p & S₁[k] ) } holds
x is natural

proof

let x be object ; :: thesis: ( x in { H₁(k) where k is Nat : ( k <= len p & S₁[k] ) } implies x is natural )
assume x in { H₁(k) where k is Nat : ( k <= len p & S₁[k] ) } ; :: thesis: x is natural
then ex n being Nat st
( x = n & n <= len p & S₁[n] ) ;
hence x is natural ; :: thesis: verum

end;

A2: { H₁(k) where k is Nat : ( k <= len p & S₁[k] ) } is finite from FINSEQ_1:sch 6();
( {} c= p & {} c= q & len {} = 0 ) ;
then 0 in { H₁(k) where k is Nat : ( k <= len p & S₁[k] ) } ;
then reconsider S = { H₁(k) where k is Nat : ( k <= len p & S₁[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₁[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;

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 A8, GRFUNC_1:2
.= R . x by A5, A10, A11, GRFUNC_1:2 ;
:: thesis: verum

end;

hence r is_a_prefix_of R by A10, GRFUNC_1:2; :: thesis: verum