let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) st not t is compound holds
ex s being SortSymbol of S ex x being Element of X . s st t = x -term
let X be V5() ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X)) st not t is compound holds
ex s being SortSymbol of S ex x being Element of X . s st t = x -term
let t be Element of (Free (S,X)); :: thesis: ( not t is compound implies ex s being SortSymbol of S ex x being Element of X . s st t = x -term )
reconsider d = t as Term of S,X by MSAFREE4:42;
assume t . {} nin [: the carrier' of S,{ the carrier of S}:] ; :: according to ABCMIZ_1:def 27 :: thesis: ex s being SortSymbol of S ex x being Element of X . s st t = x -term
then consider s being SortSymbol of S, x being Element of X . s such that
A1: d . {} = [x,s] by MSATERM:2;
take s ; :: thesis: ex x being Element of X . s st t = x -term
take x ; :: thesis: t = x -term
thus t = x -term by A1, MSATERM:5; :: thesis: verum