let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for A2 being b₁,S -terms all_vars_including inheriting_operations MSAlgebra over S holds FreeGen X is GeneratorSet of A2
let X be non-empty ManySortedSet of S; :: thesis: for A2 being X,S -terms all_vars_including inheriting_operations MSAlgebra over S holds FreeGen X is GeneratorSet of A2
let A2 be X,S -terms all_vars_including inheriting_operations MSAlgebra over S; :: thesis: FreeGen X is GeneratorSet of A2
set A = A2;
reconsider G = FreeGen X as ManySortedSubset of the Sorts of A2 by Def7;
defpred S₁[ set ] means for s being SortSymbol of S st $1 in the Sorts of A2 . s holds
$1 in the Sorts of (GenMSAlg G) . s;
A1: FreeMSA X = Free (S,X) by MSAFREE3:31;
A2: for s being SortSymbol of S
for v being Element of X . s holds S₁[ root-tree [v,s]]

proof

let s be SortSymbol of S; :: thesis: for v being Element of X . s holds S₁[ root-tree [v,s]]
let v be Element of X . s; :: thesis: S₁[ root-tree [v,s]]
reconsider t = root-tree [v,s] as Term of S,X by MSATERM:4;
let r be SortSymbol of S; :: thesis: ( root-tree [v,s] in the Sorts of A2 . r implies root-tree [v,s] in the Sorts of (GenMSAlg G) . r )
assume A3: root-tree [v,s] in the Sorts of A2 . r ; :: thesis: root-tree [v,s] in the Sorts of (GenMSAlg G) . r
the Sorts of A2 is ManySortedSubset of the Sorts of (Free (S,X)) by Def6;
then the Sorts of A2 . r c= the Sorts of (Free (S,X)) . r by PBOOLE:def 2, PBOOLE:def 18;
then t in the Sorts of (Free (S,X)) . r by A3;
then t in FreeSort (X,r) by A1, MSAFREE:def 11;
then r = the_sort_of t by MSATERM:def 5
.= s by MSATERM:14 ;
then root-tree [v,s] in FreeGen (r,X) by MSAFREE:def 15;
then A4: root-tree [v,s] in (FreeGen X) . r by MSAFREE:def 16;
FreeGen X is ManySortedSubset of the Sorts of (GenMSAlg G) by MSUALG_2:def 17;
then (FreeGen X) . r c= the Sorts of (GenMSAlg G) . r by PBOOLE:def 2, PBOOLE:def 18;
hence root-tree [v,s] in the Sorts of (GenMSAlg G) . r by A4; :: thesis: verum

end;

A5: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of S] -tree p]

proof

let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,X); :: thesis: ( ( for t being Term of S,X st t in rng p holds
S₁[t] ) implies S₁[[o, the carrier of S] -tree p] )
assume A6: for t being Term of S,X st t in rng p holds
S₁[t] ; :: thesis: S₁[[o, the carrier of S] -tree p]
let r be SortSymbol of S; :: thesis: ( [o, the carrier of S] -tree p in the Sorts of A2 . r implies [o, the carrier of S] -tree p in the Sorts of (GenMSAlg G) . r )
assume [o, the carrier of S] -tree p in the Sorts of A2 . r ; :: thesis: [o, the carrier of S] -tree p in the Sorts of (GenMSAlg G) . r
then reconsider t1 = [o, the carrier of S] -tree p as Element of the Sorts of A2 . r ;
p is SubtreeSeq of Sym (o,X) by MSATERM:def 2;
then ( Sym (o,X) ==> roots p & p is FinSequence of TS (DTConMSA X) ) by DTCONSTR:def 6;
then A7: t1 = (DenOp (o,X)) . p by MSAFREE:def 12;
p is Element of Args (o,(FreeMSA X)) by INSTALG1:1;
then p in Args (o,(FreeMSA X)) ;
then A8: p in Args (o,(Free (S,X))) by MSAFREE3:31;
then ( (Den (o,(Free (S,X)))) . p in ( the Sorts of (Free (S,X)) * the ResultSort of S) . o & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:5, FUNCT_2:def 1;
then A9: (Den (o,(Free (S,X)))) . p in the Sorts of (Free (S,X)) . (the_result_sort_of o) by FUNCT_1:13;
(Den (o,(Free (S,X)))) . p = t1 by A1, A7, MSAFREE:def 13;
then (Den (o,(Free (S,X)))) . p in the Sorts of A2 . (the_result_sort_of o) by A9, Th43;
then A10: ( p in Args (o,A2) & (Den (o,A2)) . p = (Den (o,(Free (S,X)))) . p ) by A8, Def8;
A11: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
A12: Args (o,(GenMSAlg G)) = H₁( the Sorts of (GenMSAlg G) # , the_arity_of o) by A11, FUNCT_1:13
.= product ( the Sorts of (GenMSAlg G) * (the_arity_of o)) by FINSEQ_2:def 5 ;
A13: Args (o,A2) = H₁( the Sorts of A2 # , the_arity_of o) by A11, FUNCT_1:13
.= product ( the Sorts of A2 * (the_arity_of o)) by FINSEQ_2:def 5 ;
A14: dom ( the Sorts of (GenMSAlg G) * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;
A15: dom ( the Sorts of A2 * (the_arity_of o)) = dom (the_arity_of o) by PARTFUN1:def 2;
then A16: dom p = dom (the_arity_of o) by A10, A13, CARD_3:9;

now :: thesis: for x being object st x in dom (the_arity_of o) holds
p . x in ( the Sorts of (GenMSAlg G) * (the_arity_of o)) . x

let x be object ; :: thesis: ( x in dom (the_arity_of o) implies p . x in ( the Sorts of (GenMSAlg G) * (the_arity_of o)) . x )
assume A17: x in dom (the_arity_of o) ; :: thesis: p . x in ( the Sorts of (GenMSAlg G) * (the_arity_of o)) . x
then A18: ( p . x in rng p & p . x in ( the Sorts of A2 * (the_arity_of o)) . x ) by A16, FUNCT_1:def 3, CARD_3:9, A10, A15, A13;
( (the_arity_of o) . x in rng (the_arity_of o) & rng (the_arity_of o) c= the carrier of S ) by A17, FUNCT_1:def 3;
then reconsider s = (the_arity_of o) . x as SortSymbol of S ;
reconsider px = p . x as Element of the Sorts of A2 . s by A18, A17, FUNCT_1:13;
px is Term of S,X by Th42;
then px in the Sorts of (GenMSAlg G) . s by A18, A6;
hence p . x in ( the Sorts of (GenMSAlg G) * (the_arity_of o)) . x by A17, FUNCT_1:13; :: thesis: verum

end;

then reconsider q = p as Element of Args (o,(GenMSAlg G)) by A12, A16, A14, CARD_3:9;
reconsider B = the Sorts of (GenMSAlg G) as ManySortedSubset of the Sorts of A2 by MSUALG_2:def 9;
A19: ( B is opers_closed & the Charact of (GenMSAlg G) = Opers (A2,B) ) by MSUALG_2:def 9;
A20: B is_closed_on o by MSUALG_2:def 6, MSUALG_2:def 9;
Den (o,(GenMSAlg G)) = o /. B by A19, MSUALG_2:def 8
.= (Den (o,A2)) | (((B #) * the Arity of S) . o) by A20, MSUALG_2:def 7 ;
then A21: (Den (o,(GenMSAlg G))) . p = (Den (o,A2)) . q by FUNCT_1:49;
A22: (Den (o,(GenMSAlg G))) . q = [o, the carrier of S] -tree p by A1, A21, A7, A10, MSAFREE:def 13;
then A23: [o, the carrier of S] -tree p in Result (o,(GenMSAlg G)) by FUNCT_2:5;
dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then A24: ( Result (o,(GenMSAlg G)) = the Sorts of (GenMSAlg G) . (the_result_sort_of o) & Result (o,A2) = the Sorts of A2 . (the_result_sort_of o) ) by FUNCT_1:13;
( t1 in Result (o,A2) & t1 in the Sorts of A2 . r ) by A10, A21, A22, FUNCT_2:5;
hence [o, the carrier of S] -tree p in the Sorts of (GenMSAlg G) . r by A23, A24, PROB_2:def 2, XBOOLE_0:3; :: thesis: verum

end;

A25: for t being Term of S,X holds S₁[t] from MSATERM:sch 1(A2, A5);
G is GeneratorSet of A2

proof

now :: thesis: ( the Sorts of (GenMSAlg G) c= the Sorts of A2 & the Sorts of A2 c= the Sorts of (GenMSAlg G) )

the Sorts of (GenMSAlg G) is ManySortedSubset of the Sorts of A2 by MSUALG_2:def 9;
hence the Sorts of (GenMSAlg G) c= the Sorts of A2 by PBOOLE:def 18; :: thesis: the Sorts of A2 c= the Sorts of (GenMSAlg G)
thus the Sorts of A2 c= the Sorts of (GenMSAlg G) :: thesis: verum

proof

let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in the carrier of S or the Sorts of A2 . x c= the Sorts of (GenMSAlg G) . x )
assume x in the carrier of S ; :: thesis: the Sorts of A2 . x c= the Sorts of (GenMSAlg G) . x
then reconsider s = x as SortSymbol of S ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the Sorts of A2 . x or y in the Sorts of (GenMSAlg G) . x )
assume y in the Sorts of A2 . x ; :: thesis: y in the Sorts of (GenMSAlg G) . x
then reconsider y = y as Element of the Sorts of A2 . s ;
the Sorts of A2 is ManySortedSubset of the Sorts of (Free (S,X)) by Def6;
then the Sorts of A2 . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def 2, PBOOLE:def 18;
then y is Element of the Sorts of (Free (S,X)) . s ;
then y is Element of (FreeMSA X) by MSAFREE3:31;
then y is Term of S,X by MSAFREE3:6;
hence y in the Sorts of (GenMSAlg G) . x by A25; :: thesis: verum

end;

end;

hence the Sorts of (GenMSAlg G) = the Sorts of A2 by PBOOLE:146; :: according to MSAFREE:def 4 :: thesis: verum

end;

hence FreeGen X is GeneratorSet of A2 ; :: thesis: verum