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