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 A1: 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 A2: s = (the_arity_of o) . 1 and
A3: 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;
A4: dom <*ta*> = Seg 1 by FINSEQ_1:55;
A5: dom <*s*> = Seg 1 by FINSEQ_1:55;
A6: the_arity_of o = <*s*> by A1, A2, FINSEQ_1:57;
A7: 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 A8: i = 1 by A4, 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 A9: t = <*ta*> . i ; :: thesis: the_sort_of t = (the_arity_of o) . i
A10: the Sorts of (Free C,(MSVars C)) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by A7, PBOOLE:def 23;
A11: t = a by A8, A9, FINSEQ_1:57;
A12: the Sorts of (Free C,(MSVars C)) . s c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . s by A10, PBOOLE:def 5;
t in the Sorts of (Free C,(MSVars C)) . s by A3, A11, Th41;
hence the_sort_of t = (the_arity_of o) . i by A2, A8, A12, MSAFREE3:8; :: thesis: verum

end;

then reconsider p = <*ta*> as ArgumentSeq of Sym o,((MSVars C) \/ (the carrier of C --> {0 })) by A4, A5, A6, MSATERM:25;
A13: 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 s9 = 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
A14: t in rng p and
A15: x in (C variables_in t) . s9 by MSAFREE3:12;
A16: C variables_in a c= MSVars C by MSAFREE3:28;
A17: rng p = {a} by FINSEQ_1:55;
A18: (C variables_in a) . s9 c= (MSVars C) . s9 by A16, PBOOLE:def 5;
t = a by A14, A17, TARSKI:def 1;
hence x in (MSVars C) . s by A15, A18; :: thesis: verum

end;

set s9 = the_result_sort_of o;
A19: 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 A7, 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 A13, A19;
hence [o,the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o by Th41; :: thesis: verum