let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
for A being b₁,S -terms MSAlgebra over S
for t being Element of A holds t is Term of S,X
let X be V5() ManySortedSet of S; :: thesis: for A being X,S -terms MSAlgebra over S
for t being Element of A holds t is Term of S,X
let A be X,S -terms MSAlgebra over S; :: thesis: for t being Element of A holds t is Term of S,X
let t be Element of A; :: thesis: t is Term of S,X
consider s being object such that
A1: ( s in dom the Sorts of A & t in the Sorts of A . s ) by CARD_5:2;
reconsider s = s as SortSymbol of S by A1;
the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) by Def6;
then the Sorts of A . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def 2, PBOOLE:def 18;
then t is Element of the Sorts of (Free (S,X)) . s by A1;
then t is Element of (FreeMSA X) by MSAFREE3:31;
hence t is Term of S,X by MSAFREE3:6; :: thesis: verum