let mm be Element of NAT ; :: thesis: for S being Language holds (S -termsOfMaxDepth) . mm c= AllTermsOf S
let S be Language; :: thesis: (S -termsOfMaxDepth) . mm c= AllTermsOf S
set T = S -termsOfMaxDepth ;
dom (S -termsOfMaxDepth) = NAT by Def30;
hence (S -termsOfMaxDepth) . mm c= AllTermsOf S by ZFMISC_1:74, FUNCT_1:3; :: thesis: verum