let S be non empty non void ManySortedSign ; :: thesis: for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V st not t is root holds
t is CompoundTerm of S,V
let V be V2() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,V st not t is root holds
t is CompoundTerm of S,V
let t be Term of S,V; :: thesis: ( not t is root implies t is CompoundTerm of S,V )
assume A1: not t is root ; :: thesis: t is CompoundTerm of S,V
per cases ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] ) by Th2;
suppose ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] ; :: thesis: t is CompoundTerm of S,V
then consider s being SortSymbol of S, x being Element of V . s such that
A2: t . {} = [x,s] ;
t = root-tree [x,s] by A2, Th5;
hence t is CompoundTerm of S,V by A1; :: thesis: verum
end;
suppose t . {} in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: t is CompoundTerm of S,V
hence t . {} in [: the carrier' of S,{ the carrier of S}:] ; :: according to MSATERM:def 6 :: thesis: verum
end;
end;