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
for s being SortSymbol of S st t in the Sorts of (Free (S,X)) . s holds
t in the Sorts of A . s
let X be V5() ManySortedSet of S; :: thesis: for A being X,S -terms MSAlgebra over S
for t being Element of A
for s being SortSymbol of S st t in the Sorts of (Free (S,X)) . s holds
t in the Sorts of A . s
let A be X,S -terms MSAlgebra over S; :: thesis: for t being Element of A
for s being SortSymbol of S st t in the Sorts of (Free (S,X)) . s holds
t in the Sorts of A . s
let t be Element of A; :: thesis: for s being SortSymbol of S st t in the Sorts of (Free (S,X)) . s holds
t in the Sorts of A . s
consider x being object such that
A1: ( x in dom the Sorts of A & t in the Sorts of A . x ) by CARD_5:2;
reconsider x = x as SortSymbol of S by A1;
the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) by Def6;
then A2: the Sorts of A . x c= the Sorts of (Free (S,X)) . x by PBOOLE:def 2, PBOOLE:def 18;
let s be SortSymbol of S; :: thesis: ( t in the Sorts of (Free (S,X)) . s implies t in the Sorts of A . s )
assume t in the Sorts of (Free (S,X)) . s ; :: thesis: t in the Sorts of A . s
hence t in the Sorts of A . s by A1, A2, XBOOLE_0:3, PROB_2:def 2; :: thesis: verum