let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for A1 being b1,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 V5() ManySortedSet of S; 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; for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))
let o be OperSymbol of S; Args (o,A1) c= Args (o,(Free (S,X)))
let x be object ; TARSKI:def 3 ( not x in Args (o,A1) or x in Args (o,(Free (S,X))) )
assume
x in Args (o,A1)
; 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 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)) . alet a be
object ;
( 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)
;
( the Sorts of A1 * (the_arity_of o)) . a c= ( the Sorts of (Free (S,X)) * (the_arity_of o)) . athen 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;
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; verum