let C be initialized ConstructorSignature; for o being OperSymbol of C st len (the_arity_of o) = 2 holds
for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o
let o be OperSymbol of C; ( len (the_arity_of o) = 2 implies for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o )
assume A1:
len (the_arity_of o) = 2
; for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o
set X = MSVars C;
set Y = (MSVars C) (\/) ( the carrier of C --> {0});
let a, b be expression of C; ( ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) implies [o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o )
given s1, s2 being SortSymbol of C such that A2:
s1 = (the_arity_of o) . 1
and
A3:
s2 = (the_arity_of o) . 2
and
A4:
a is expression of C,s1
and
A5:
b is expression of C,s2
; [o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o
reconsider ta = a, tb = b as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
A6:
dom <*ta,tb*> = Seg 2
by FINSEQ_1:89;
A7:
dom <*s1,s2*> = Seg 2
by FINSEQ_1:89;
A8:
the_arity_of o = <*s1,s2*>
by A1, A2, A3, FINSEQ_1:44;
A9:
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,tb*> holds
for t being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st t = <*ta,tb*> . i holds
the_sort_of t = (the_arity_of o) . ilet i be
Nat;
( i in dom <*ta,tb*> implies for t being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st t = <*ta,tb*> . i holds
the_sort_of t = (the_arity_of o) . i )assume
i in dom <*ta,tb*>
;
for t being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st t = <*ta,tb*> . i holds
the_sort_of t = (the_arity_of o) . ithen A10:
(
i = 1 or
i = 2 )
by A6, FINSEQ_1:2, TARSKI:def 2;
let t be
Term of
C,
((MSVars C) (\/) ( the carrier of C --> {0}));
( t = <*ta,tb*> . i implies the_sort_of t = (the_arity_of o) . i )assume A11:
t = <*ta,tb*> . i
;
the_sort_of t = (the_arity_of o) . iA12:
the
Sorts of
(Free (C,(MSVars C))) c= the
Sorts of
(FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0})))
by A9, PBOOLE:def 18;
A13:
( (
i = 1 &
t = a ) or (
i = 2 &
t = b ) )
by A10, A11, FINSEQ_1:44;
A14:
the
Sorts of
(Free (C,(MSVars C))) . s1 c= the
Sorts of
(FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . s1
by A12;
A15:
the
Sorts of
(Free (C,(MSVars C))) . s2 c= the
Sorts of
(FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . s2
by A12;
( (
i = 1 &
t in the
Sorts of
(Free (C,(MSVars C))) . s1 ) or (
i = 2 &
t in the
Sorts of
(Free (C,(MSVars C))) . s2 ) )
by A4, A5, A13, Th41;
hence
the_sort_of t = (the_arity_of o) . i
by A2, A3, A14, A15, MSAFREE3:7;
verum end;
then reconsider p = <*ta,tb*> as ArgumentSeq of Sym (o,((MSVars C) (\/) ( the carrier of C --> {0}))) by A6, A7, A8, MSATERM:25;
A16:
variables_in ((Sym (o,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p) c= MSVars C
set s9 = the_result_sort_of o;
A24:
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 A9, MSAFREE3:def 5;
then
[o, the carrier of C] -tree <*a,b*> in the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o)
by A16, A24;
hence
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o
by Th41; verum