let C be initialized ConstructorSignature; :: thesis: for c being constructor OperSymbol of C
for p being DTree-yielding FinSequence holds
( [c,the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
let c be constructor OperSymbol of C; :: thesis: for p being DTree-yielding FinSequence holds
( [c,the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
set o = c;
A0: ( c <> * & c <> non_op ) by CNSTR2;
let p be DTree-yielding FinSequence; :: thesis: ( [c,the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
set V = (MSVars C) \/ (the carrier of C --> {0 });
BB: the Sorts of (Free C,(MSVars C)) = C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:25;

hereby :: thesis: ( len p = len (the_arity_of c) & p in (QuasiTerms C) * implies [c,the carrier of C] -tree p is expression of C )

assume A2: [c,the carrier of C] -tree p is expression of C ; :: thesis: ( len p = len (the_arity_of c) & p in (QuasiTerms C) * )
then CC: [c,the carrier of C] -tree p is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
then A3: p is ArgumentSeq of Sym c,((MSVars C) \/ (the carrier of C --> {0 })) by MSATERM:1;
hence len p = len (the_arity_of c) by MSATERM:22; :: thesis: p in (QuasiTerms C) *
reconsider q = p as ArgumentSeq of Sym c,((MSVars C) \/ (the carrier of C --> {0 })) by CC, MSATERM:1;
A5: the_sort_of ((Sym c,((MSVars C) \/ (the carrier of C --> {0 }))) -tree q) = the_result_sort_of c by MSATERM:20;
A6: variables_in ((Sym c,((MSVars C) \/ (the carrier of C --> {0 }))) -tree q) c= MSVars C by A2, MSAFREE3:28;
(C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (the_result_sort_of c) = { t where t is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) : ( the_sort_of t = the_result_sort_of c & variables_in t c= MSVars C ) } by MSAFREE3:def 6;
then (Sym c,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (the_result_sort_of c) by A5, A6;
then A4: rng p c= Union (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) by A3, MSAFREE3:20;
rng p c= QuasiTerms C

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng p or a in QuasiTerms C )
assume B0: a in rng p ; :: thesis: a in QuasiTerms C
then reconsider ta = a as expression of C by A4, MSAFREE3:25;
consider i being set such that
B1: ( i in dom p & a = p . i ) by B0, FUNCT_1:def 5;
reconsider i = i as Nat by B1;
reconsider t = p . i as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by A3, B1, MSATERM:22;
the Arity of C . c in {a_Term } * by A0, CONSTRSIGN;
then ( dom p = dom (the_arity_of c) & the_arity_of c is FinSequence of {a_Term } ) by A3, FINSEQ_1:def 11, MSATERM:22;
then ( (the_arity_of c) . i in rng (the_arity_of c) & rng (the_arity_of c) c= {(a_Term C)} ) by B1, FINSEQ_1:def 4, FUNCT_1:def 5;
then (the_arity_of c) . i = a_Term C by TARSKI:def 1;
then B2: the_sort_of t = a_Term C by A3, B1, MSATERM:23;
t = ta by B1;
then variables_in t c= MSVars C by MSAFREE3:28;
then t in { T where T is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) : ( the_sort_of T = a_Term C & variables_in T c= MSVars C ) } by B2;
then t in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Term C) by MSAFREE3:def 6;
hence a in QuasiTerms C by B1, MSAFREE3:24; :: thesis: verum

end;

then p is FinSequence of QuasiTerms C by FINSEQ_1:def 4;
hence p in (QuasiTerms C) * by FINSEQ_1:def 11; :: thesis: verum

end;

assume A3: len p = len (the_arity_of c) ; :: thesis: ( not p in (QuasiTerms C) * or [c,the carrier of C] -tree p is expression of C )
assume A4: p in (QuasiTerms C) * ; :: thesis: [c,the carrier of C] -tree p is expression of C
( C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 })) is opers_closed & Free C,(MSVars C) = (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) | (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) ) by MSAFREE3:22, MSAFREE3:26;
then the Sorts of (Free C,(MSVars C)) is ManySortedSubset of the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by MSUALG_2:def 10;
then the Sorts of (Free C,(MSVars C)) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by PBOOLE:def 23;
then A7: QuasiTerms C c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Term C) by PBOOLE:def 5;
0B: p is FinSequence of QuasiTerms C by A4, FINSEQ_1:def 11;
then B0: rng p c= QuasiTerms C by FINSEQ_1:def 4;

now

let i be Nat; :: thesis: ( i in dom p implies ex T being Term of C,((MSVars C) \/ (the carrier of C --> {0 })) st
( T = p . i & the_sort_of T = (the_arity_of c) . i ) )
assume B1: i in dom p ; :: thesis: ex T being Term of C,((MSVars C) \/ (the carrier of C --> {0 })) st
( T = p . i & the_sort_of T = (the_arity_of c) . i )
then p . i in rng p by FUNCT_1:def 5;
then B3: p . i in QuasiTerms C by B0;
then reconsider t = p . i as expression of C ;
the Arity of C . c in {a_Term } * by A0, CONSTRSIGN;
then ( dom p = dom (the_arity_of c) & the_arity_of c is FinSequence of {a_Term } ) by A3, FINSEQ_1:def 11, FINSEQ_3:31;
then ( (the_arity_of c) . i in rng (the_arity_of c) & rng (the_arity_of c) c= {(a_Term C)} ) by B1, FINSEQ_1:def 4, FUNCT_1:def 5;
then B2: (the_arity_of c) . i = a_Term C by TARSKI:def 1;
reconsider T = t as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
take T = T; :: thesis: ( T = p . i & the_sort_of T = (the_arity_of c) . i )
thus T = p . i ; :: thesis: the_sort_of T = (the_arity_of c) . i
T in the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Term C) by B3, A7;
then T in FreeSort ((MSVars C) \/ (the carrier of C --> {0 })),(a_Term C) by MSAFREE:def 13;
hence the_sort_of T = (the_arity_of c) . i by B2, MSATERM:def 5; :: thesis: verum

end;

then A5: p is ArgumentSeq of Sym c,((MSVars C) \/ (the carrier of C --> {0 })) by A3, MSATERM:24;
A6: dom the Sorts of (Free C,(MSVars C)) = the carrier of C by PARTFUN1:def 4;
rng p c= Union (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) by BB, 0B, FINSEQ_1:def 4;
then (Sym c,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (the_result_sort_of c) by A5, MSAFREE3:20;
hence [c,the carrier of C] -tree p is expression of C by BB, A6, CARD_5:10; :: thesis: verum