let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s
let s be SortSymbol of S; :: thesis: for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s
let e be Element of (Equations S) . s; :: thesis: e `2 in the Sorts of (TermAlg S) . s
set T = the Sorts of (TermAlg S);
e is Element of [:( the Sorts of (TermAlg S) . s),( the Sorts of (TermAlg S) . s):] by PBOOLE:def 16;
hence e `2 in the Sorts of (TermAlg S) . s by MCART_1:10; :: thesis: verum