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 holds
( ( for t being Element of A holds t is Element of (Free (S,X)) ) & ( for s being SortSymbol of S
for t being Element of A,s holds t is Element of (Free (S,X)),s ) )
let X be V5() ManySortedSet of S; :: thesis: for A being X,S -terms MSAlgebra over S holds
( ( for t being Element of A holds t is Element of (Free (S,X)) ) & ( for s being SortSymbol of S
for t being Element of A,s holds t is Element of (Free (S,X)),s ) )
let A be X,S -terms MSAlgebra over S; :: thesis: ( ( for t being Element of A holds t is Element of (Free (S,X)) ) & ( for s being SortSymbol of S
for t being Element of A,s holds t is Element of (Free (S,X)),s ) )
A1: the Sorts of A is MSSubset of (Free (S,X)) by Def6;
then Union the Sorts of A c= Union the Sorts of (Free (S,X)) by Th1, PBOOLE:def 18;
hence for t being Element of A holds t is Element of (Free (S,X)) ; :: thesis: for s being SortSymbol of S
for t being Element of A,s holds t is Element of (Free (S,X)),s
let s be SortSymbol of S; :: thesis: for t being Element of A,s holds t is Element of (Free (S,X)),s
let t be Element of A,s; :: thesis: t is Element of (Free (S,X)),s
( t in the Sorts of A . s & the Sorts of A . s c= the Sorts of (Free (S,X)) . s ) by A1, PBOOLE:def 2, PBOOLE:def 18;
hence t is Element of (Free (S,X)),s ; :: thesis: verum