let C be initialized ConstructorSignature; :: thesis: for o being OperSymbol of C st len (the_arity_of o) = 1 holds
for a being expression of C st ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & a is expression of C,s ) holds
[o,the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o
let o be OperSymbol of C; :: thesis: ( len (the_arity_of o) = 1 implies for a being expression of C st ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & a is expression of C,s ) holds
[o,the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o )
assume A: len (the_arity_of o) = 1 ; :: thesis: for a being expression of C st ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & a is expression of C,s ) holds
[o,the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o
set X = MSVars C;
set Y = (MSVars C) \/ (the carrier of C --> {0 });
let a be expression of C; :: thesis: ( ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & a is expression of C,s ) implies [o,the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o )
given s being SortSymbol of C such that A0: ( s = (the_arity_of o) . 1 & a is expression of C,s ) ; :: thesis: [o,the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o
reconsider ta = a as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
A2: ( dom <*ta*> = Seg 1 & dom <*s*> = Seg 1 ) by FINSEQ_1:55;
A4: the_arity_of o = <*s*> by A, A0, FINSEQ_1:57;
B1: the Sorts of (Free C,(MSVars C)) = C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:25;

now

let i be Nat; :: thesis: ( i in dom <*ta*> implies for t being Term of C,((MSVars C) \/ (the carrier of C --> {0 })) st t = <*ta*> . i holds
the_sort_of t = (the_arity_of o) . i )
assume i in dom <*ta*> ; :: thesis: for t being Term of C,((MSVars C) \/ (the carrier of C --> {0 })) st t = <*ta*> . i holds
the_sort_of t = (the_arity_of o) . i
then A3: i = 1 by A2, FINSEQ_1:4, TARSKI:def 1;
let t be Term of C,((MSVars C) \/ (the carrier of C --> {0 })); :: thesis: ( t = <*ta*> . i implies the_sort_of t = (the_arity_of o) . i )
assume t = <*ta*> . i ; :: thesis: the_sort_of t = (the_arity_of o) . i
then ( the Sorts of (Free C,(MSVars C)) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) & t = a ) by B1, A3, FINSEQ_1:57, PBOOLE:def 23;
then ( the Sorts of (Free C,(MSVars C)) . s c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . s & t in the Sorts of (Free C,(MSVars C)) . s ) by A0, Th42, PBOOLE:def 5;
hence the_sort_of t = (the_arity_of o) . i by A0, A3, MSAFREE3:8; :: thesis: verum

end;

then reconsider p = <*ta*> as ArgumentSeq of Sym o,((MSVars C) \/ (the carrier of C --> {0 })) by A2, A4, MSATERM:25;
A5: variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p) c= MSVars C

proof

let s be set ; :: according to PBOOLE:def 5 :: thesis: ( not s in the carrier of C or (variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p)) . s c= (MSVars C) . s )
assume s in the carrier of C ; :: thesis: (variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p)) . s c= (MSVars C) . s
then reconsider s' = s as SortSymbol of C ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p)) . s or x in (MSVars C) . s )
assume x in (variables_in ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p)) . s ; :: thesis: x in (MSVars C) . s
then consider t being DecoratedTree such that
B2: ( t in rng p & x in (C variables_in t) . s' ) by MSAFREE3:12;
( C variables_in a c= MSVars C & rng p = {a} ) by FINSEQ_1:55, MSAFREE3:28;
then ( (C variables_in a) . s' c= (MSVars C) . s' & t = a ) by B2, PBOOLE:def 5, TARSKI:def 1;
hence x in (MSVars C) . s by B2; :: thesis: verum

end;

set s' = the_result_sort_of o;
A7: the_sort_of ((Sym o,((MSVars C) \/ (the carrier of C --> {0 }))) -tree p) = the_result_sort_of o by MSATERM:20;
the Sorts of (Free C,(MSVars C)) . (the_result_sort_of o) = { t where t is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) : ( the_sort_of t = the_result_sort_of o & variables_in t c= MSVars C ) } by B1, MSAFREE3:def 6;
then [o,the carrier of C] -tree <*a*> in the Sorts of (Free C,(MSVars C)) . (the_result_sort_of o) by A5, A7;
hence [o,the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o by Th42; :: thesis: verum