let S be Language; AllTermsOf S is S -prefix
set SS = AllSymbolsOf S;
set f = (AllSymbolsOf S) -concatenation ;
set F = (AllSymbolsOf S) -multiCat ;
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
now for t1, t2, w1, w2 being set st t1 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & t2 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . (t1,w1) = ((AllSymbolsOf S) -concatenation) . (t2,w2) holds
( t1 = t2 & w1 = w2 )let t1,
t2,
w1,
w2 be
set ;
( t1 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & t2 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) & w1 in (AllSymbolsOf S) * & w2 in (AllSymbolsOf S) * & ((AllSymbolsOf S) -concatenation) . (t1,w1) = ((AllSymbolsOf S) -concatenation) . (t2,w2) implies ( t1 = t2 & w1 = w2 ) )assume A1:
(
t1 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) &
t2 in (AllTermsOf S) /\ ((AllSymbolsOf S) *) &
w1 in (AllSymbolsOf S) * &
w2 in (AllSymbolsOf S) * &
((AllSymbolsOf S) -concatenation) . (
t1,
w1)
= ((AllSymbolsOf S) -concatenation) . (
t2,
w2) )
;
( t1 = t2 & w1 = w2 )consider mm being
Element of
NAT such that A2:
t1 in (S -termsOfMaxDepth) . mm
by Lm6, A1;
consider nn being
Element of
NAT such that A3:
t2 in (S -termsOfMaxDepth) . nn
by Lm6, A1;
set p =
mm + nn;
A4:
(S -termsOfMaxDepth) . (mm + nn) is
(AllSymbolsOf S) -concatenation -unambiguous
by FOMODEL0:def 3;
(
(S -termsOfMaxDepth) . mm c= (S -termsOfMaxDepth) . (mm + nn) &
(S -termsOfMaxDepth) . nn c= (S -termsOfMaxDepth) . (mm + nn) )
by Lm5;
then
(
t1 in ((S -termsOfMaxDepth) . (mm + nn)) /\ ((AllSymbolsOf S) *) &
t2 in ((S -termsOfMaxDepth) . (mm + nn)) /\ ((AllSymbolsOf S) *) &
w1 in (AllSymbolsOf S) * &
w2 in (AllSymbolsOf S) * &
((AllSymbolsOf S) -concatenation) . (
t1,
w1)
= ((AllSymbolsOf S) -concatenation) . (
t2,
w2) )
by A1, XBOOLE_0:def 4, A2, A3;
hence
(
t1 = t2 &
w1 = w2 )
by A4;
verum end;
then
AllTermsOf S is AllSymbolsOf S -prefix
by FOMODEL0:def 10;
hence
AllTermsOf S is S -prefix
; verum