let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for A1 being b₁,S -terms all_vars_including MSAlgebra over S
for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))
let X be non-empty ManySortedSet of S; :: thesis: for A1 being X,S -terms all_vars_including MSAlgebra over S
for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))
let A1 be X,S -terms all_vars_including MSAlgebra over S; :: thesis: for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))
let o be OperSymbol of S; :: thesis: Args (o,A1) c= Args (o,(Free (S,X)))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Args (o,A1) or x in Args (o,(Free (S,X))) )
assume x in Args (o,A1) ; :: thesis: x in Args (o,(Free (S,X)))
then A1: x in product ( the Sorts of A1 * (the_arity_of o)) by PRALG_2:3;
A2: dom ( the Sorts of A1 * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3;
A3: dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o) by PRALG_2:3;

now :: thesis: for a being object st a in dom (the_arity_of o) holds
( the Sorts of A1 * (the_arity_of o)) . a c= ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a

let a be object ; :: thesis: ( a in dom (the_arity_of o) implies ( the Sorts of A1 * (the_arity_of o)) . a c= ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a )
assume A4: a in dom (the_arity_of o) ; :: thesis: ( the Sorts of A1 * (the_arity_of o)) . a c= ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a
then A5: (the_arity_of o) . a in the carrier of S by FUNCT_1:102;
A6: ( the Sorts of A1 * (the_arity_of o)) . a = the Sorts of A1 . ((the_arity_of o) . a) by A4, FUNCT_1:13;
A7: ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a = the Sorts of (Free (S,X)) . ((the_arity_of o) . a) by A4, FUNCT_1:13;
the Sorts of A1 is MSSubset of (Free (S,X)) by Def6;
hence ( the Sorts of A1 * (the_arity_of o)) . a c= ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a by A5, A6, A7, PBOOLE:def 2, PBOOLE:def 18; :: thesis: verum

end;

then product ( the Sorts of A1 * (the_arity_of o)) c= product ( the Sorts of (Free (S,X)) * (the_arity_of o)) by A2, A3, CARD_3:27;
then x in product ( the Sorts of (Free (S,X)) * (the_arity_of o)) by A1;
hence x in Args (o,(Free (S,X))) by PRALG_2:3; :: thesis: verum