let C be initialized ConstructorSignature; :: thesis: 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; :: thesis: ( 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 A: len (the_arity_of o) = 2 ; :: thesis: 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; :: thesis: ( 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 A0: ( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) ; :: thesis: [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:9;
A2: ( dom <*ta,tb*> = Seg 2 & dom <*s1,s2*> = Seg 2 ) by FINSEQ_3:29;
A4: the_arity_of o = <*s1,s2*> by A, A0, FINSEQ_1:61;
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,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*> ; :: thesis: 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
then A3: ( i = 1 or i = 2 ) by A2, FINSEQ_1:4, TARSKI:def 2;
let t be Term of C,((MSVars C) \/ (the carrier of C --> {0 })); :: thesis: ( t = <*ta,tb*> . i implies the_sort_of t = (the_arity_of o) . i )
assume t = <*ta,tb*> . 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 }))) & ( ( i = 1 & t = a ) or ( i = 2 & t = b ) ) ) by B1, A3, FINSEQ_1:61, PBOOLE:def 23;
then ( the Sorts of (Free C,(MSVars C)) . s1 c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . s1 & the Sorts of (Free C,(MSVars C)) . s2 c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . s2 & ( ( 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 A0, Th42, PBOOLE:def 5;
hence the_sort_of t = (the_arity_of o) . i by A0, MSAFREE3:8; :: thesis: verum

end;

then reconsider p = <*ta,tb*> 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 & C variables_in b c= MSVars C & rng p = {a,b} ) by FINSEQ_2:147, MSAFREE3:28;
then ( (C variables_in a) . s' c= (MSVars C) . s' & (C variables_in b) . s' c= (MSVars C) . s' & ( t = a or t = b ) ) by B2, PBOOLE:def 5, TARSKI:def 2;
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,b*> in the Sorts of (Free C,(MSVars C)) . (the_result_sort_of o) by A5, A7;
hence [o,the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o by Th42; :: thesis: verum