set IT = (x,y) -SymbolSubstIn p;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
dom ((x,y) -SymbolSubstIn p) = dom p by FUNCT_4:99
.= Seg (len p) by FINSEQ_1:def 3
.= Seg mm by CARD_1:def 7 ;
then len ((x,y) -SymbolSubstIn p) = mm by FINSEQ_1:def 3;
hence for b₁ being FinSequence st b₁ = (x,y) -SymbolSubstIn p holds
b₁ is m -element by CARD_1:def 7; :: thesis: verum