let C be initialized ConstructorSignature; 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; ( 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
; 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; ( 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
; [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 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) . ilet i be
Nat;
( 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*>
;
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) . ithen A8:
i = 1
by A4, FINSEQ_1:2, TARSKI:def 1;
let t be
Term of
C,
((MSVars C) (\/) ( the carrier of C --> {0}));
( t = <*ta*> . i implies the_sort_of t = (the_arity_of o) . i )assume A9:
t = <*ta*> . i
;
the_sort_of t = (the_arity_of o) . iA10:
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, FINSEQ_1:40;
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;
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
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; verum