let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of S
for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V holds t is c-Term of A,V
let A be MSAlgebra of S; :: thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V holds t is c-Term of A,V
let V be V16() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,V holds t is c-Term of A,V
V c= the Sorts of A \/ V by PBOOLE:14;
hence for t being Term of S,V holds t is c-Term of A,V by Th26; :: thesis: verum