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 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;
hence r is_a_prefix_of R by A10, GRFUNC_1:2; :: thesis: verum