let S be non empty non void ManySortedSign ; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
let Y be ManySortedSubset of X; :: thesis:
thus A1: the Sorts of (Free (S,Y)) c= the Sorts of (Free (S,X)) :: according to MSUALG_2:def 9,PBOOLE:def 18 :: thesis:

proof

let x be object ; :: according to PBOOLE:def 2 :: thesis:
assume x in the carrier of S ; :: thesis:
then reconsider s = x as SortSymbol of S ;
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: z in the Sorts of (Free (S,Y)) . x ; :: thesis:
then reconsider t = z as Element of the Sorts of (Free (S,Y)) . x ;
A3: t in (S -Terms (Y,(Y (\/) ( the carrier of S --> {0})))) . s by A2, MSAFREE3:24;
then reconsider t1 = t as Term of S,(Y (\/) ( the carrier of S --> {0})) by MSAFREE3:16;
A4: ( t = t1 & the_sort_of t1 = x & variables_in t1 c= Y ) by A3, MSAFREE3:17;
A5: Y c= X by PBOOLE:def 18;
Y (\/) ( the carrier of S --> {0}) c= X (\/) ( the carrier of S --> {0}) by PBOOLE:18, PBOOLE:def 18;
then reconsider t2 = t1 as Term of S,(X (\/) ( the carrier of S --> {0})) by MSATERM:26;
variables_in t2 = S variables_in t2 by MSAFREE3:def 4
.= variables_in t1 by MSAFREE3:def 4 ;
then ( variables_in t2 c= X & the_sort_of t2 = the_sort_of t1 ) by A4, A5, PBOOLE:13, MSAFREE3:29;
then t2 in { t3 where t3 is Term of S,(X (\/) ( the carrier of S --> {0})) : ( the_sort_of t3 = s & variables_in t3 c= X ) } by A4;
then t2 in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s by MSAFREE3:def 5;
hence z in the Sorts of (Free (S,X)) . x by MSAFREE3:24; :: thesis:

end;

let B be MSSubset of (Free (S,X)); :: thesis:
assume A6: B = the Sorts of (Free (S,Y)) ; :: thesis:
consider A1 being MSSubset of (FreeMSA (Y (\/) ( the carrier of S --> {0}))) such that
A7: ( Free (S,Y) = GenMSAlg A1 & A1 = (Reverse (Y (\/) ( the carrier of S --> {0}))) "" Y ) by MSAFREE3:def 1;
thus A8: B is opers_closed :: thesis:

proof

let o be OperSymbol of S; :: according to MSUALG_2:def 6 :: thesis:
let z be object ; :: according to TARSKI:def 3,MSUALG_2:def 5 :: thesis:
assume z in rng ((Den (o,(Free (S,X)))) | (((B #) * the Arity of S) . o)) ; :: thesis:
then consider a being object such that
A9: ( a in dom ((Den (o,(Free (S,X)))) | (((B #) * the Arity of S) . o)) & z = ((Den (o,(Free (S,X)))) | (((B #) * the Arity of S) . o)) . a ) by FUNCT_1:def 3;
A10: a in (dom (Den (o,(Free (S,X))))) /\ (((B #) * the Arity of S) . o) by A9, RELAT_1:61;
then A11: ( a in dom (Den (o,(Free (S,X)))) & a in ((B #) * the Arity of S) . o ) by XBOOLE_0:def 4;
reconsider a = a as Element of Args (o,(Free (S,X))) by A10;
A12: ((B #) * the Arity of S) . o = (B #) . (the_arity_of o) by FUNCT_2:15;
A13: (B #) . (the_arity_of o) = product (B * (the_arity_of o)) by FINSEQ_2:def 5;
A14: ( Args (o,(Free (S,X))) = product ( the Sorts of (Free (S,X)) * (the_arity_of o)) & dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o) & Args (o,(Free (S,Y))) = product ( the Sorts of (Free (S,Y)) * (the_arity_of o)) & dom ( the Sorts of (Free (S,Y)) * (the_arity_of o)) = dom (the_arity_of o) ) by PRALG_2:3;
then A15: dom a = dom (the_arity_of o) by PARTFUN1:def 2;
z = (Den (o,(Free (S,X)))) . a by A9, A11, FUNCT_1:49;
then A16: z = (Sym (o,X)) -tree a by Th13;
A17: for x being object st x in dom ( the Sorts of (Free (S,Y)) * (the_arity_of o)) holds
a . x in ( the Sorts of (Free (S,Y)) * (the_arity_of o)) . x by A11, A12, A13, A6, CARD_3:9;
then A18: a in Args (o,(Free (S,Y))) by A14, A15, CARD_3:9;
A19: (Den (o,(Free (S,Y)))) . a = [o, the carrier of S] -tree a by A17, A14, A15, CARD_3:9, Th13;
thus z in (B * the ResultSort of S) . o by A6, A16, A18, A19, FUNCT_2:5, MSUALG_6:def 1; :: thesis:

end;

now :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Args (o,(Free (S,Y))) ; :: thesis:
then A24: ( x in product ( the Sorts of (Free (S,Y)) * (the_arity_of o)) & dom ( the Sorts of (Free (S,Y)) * (the_arity_of o)) = dom (the_arity_of o) & dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o) ) by PRALG_2:3;
then consider f being Function such that
A25: ( x = f & dom f = dom (the_arity_of o) & ( for y being object st y in dom (the_arity_of o) holds
f . y in ( the Sorts of (Free (S,Y)) * (the_arity_of o)) . y ) ) by CARD_3:def 5;

now :: thesis:

let y be object ; :: thesis:
assume A26: y in dom (the_arity_of o) ; :: thesis:
( f . y in ( the Sorts of (Free (S,Y)) * (the_arity_of o)) . y & (the_arity_of o) . y in the carrier of S ) by A25, A26, FUNCT_1:102;
then ( f . y in the Sorts of (Free (S,Y)) . ((the_arity_of o) . y) & the Sorts of (Free (S,Y)) . ((the_arity_of o) . y) c= the Sorts of (Free (S,X)) . ((the_arity_of o) . y) ) by A1, A26, FUNCT_1:13;
then f . y in the Sorts of (Free (S,X)) . ((the_arity_of o) . y) ;
hence f . y in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . y by A26, FUNCT_1:13; :: thesis:

end;

then x in product ( the Sorts of (Free (S,X)) * (the_arity_of o)) by A25, A24, CARD_3:def 5;
hence x in Args (o,(Free (S,X))) by PRALG_2:3; :: thesis:

end;

dom (Den (o,(Free (S,X)))) = Args (o,(Free (S,X))) by FUNCT_2:def 1;
then A27: dom ((Den (o,(Free (S,X)))) | (Args (o,(Free (S,Y))))) = Args (o,(Free (S,Y))) by A23, RELAT_1:62;

A28: now :: thesis:

let x be object ; :: thesis:
assume A29: x in Args (o,(Free (S,Y))) ; :: thesis:
then A30: x in product ( the Sorts of (Free (S,Y)) * (the_arity_of o)) by PRALG_2:3;
reconsider p = x as Element of product ( the Sorts of (Free (S,Y)) * (the_arity_of o)) by A29, PRALG_2:3;
( dom p = dom ( the Sorts of (Free (S,Y)) * (the_arity_of o)) & rng (the_arity_of o) c= the carrier of S & dom the Sorts of (Free (S,Y)) = the carrier of S ) by A30, CARD_3:9, PARTFUN1:def 2;
then dom p = dom (the_arity_of o) by RELAT_1:27;
then dom p = Seg (len (the_arity_of o)) by FINSEQ_1:def 3;
then reconsider p = x as FinSequence by FINSEQ_1:def 2;
A31: ((Den (o,(Free (S,X)))) | (Args (o,(Free (S,Y))))) . x = (Den (o,(Free (S,X)))) . x by A29, FUNCT_1:49
.= [o, the carrier of S] -tree p by A23, A29, Th13 ;
thus ((Den (o,(Free (S,(Y (\/) ( the carrier of S --> {0})))))) | (Args (o,(Free (S,Y))))) . x = (Den (o,(Free (S,(Y (\/) ( the carrier of S --> {0})))))) . x by A29, FUNCT_1:49
.= ((Den (o,(Free (S,X)))) | (Args (o,(Free (S,Y))))) . x by A21, A29, A31, Th13 ; :: thesis:

end;

thus the Charact of (Free (S,Y)) . o = (Opers ((FreeMSA (Y (\/) ( the carrier of S --> {0}))),A2)) . o by A7, MSUALG_2:def 9
.= o /. A2 by MSUALG_2:def 8
.= (Den (o,(FreeMSA (Y (\/) ( the carrier of S --> {0}))))) | (((A2 #) * the Arity of S) . o) by A20, MSUALG_2:def 7
.= (Den (o,(Free (S,(Y (\/) ( the carrier of S --> {0})))))) | (((A2 #) * the Arity of S) . o) by MSAFREE3:31
.= (Den (o,(Free (S,X)))) | (((B #) * the Arity of S) . o) by A6, A28, A27, A22
.= o /. B by A8, MSUALG_2:def 7 ; :: thesis:

end;

hence the Charact of (Free (S,Y)) = Opers ((Free (S,X)),B) by A6, MSUALG_2:def 8; :: thesis: