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:8;
A4: dom <*ta*> = Seg 1 by FINSEQ_1:38;
A5: dom <*s*> = Seg 1 by FINSEQ_1:38;
A6: the_arity_of o = <*s*> by A1, A2, FINSEQ_1:40;
A7: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) by MSAFREE3:24;

now :: thesis: for i being Nat st i in dom <*ta*> holds
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

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:2, 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 18;
A11: t = a by A8, A9;
A12: the Sorts of (Free (C,(MSVars C))) . s c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . s by A10;
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:7; :: 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 object ; :: according to PBOOLE:def 2 :: 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 object ; :: 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:11;
A16: C variables_in a c= MSVars C by MSAFREE3:27;
A17: rng p = {a} by FINSEQ_1:38;
A18: (C variables_in a) . s9 c= (MSVars C) . s9 by A16;
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 5;
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