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