let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
let X be V5() ManySortedSet of the carrier of S; for t being Element of (Free (S,X)) holds
( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
let t be Element of (Free (S,X)); ( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )
reconsider u = t as Term of S,X by MSAFREE4:42;
per cases
( ex s being SortSymbol of S ex x being Element of X . s st u . {} = [x,s] or u . {} in [: the carrier' of S,{ the carrier of S}:] )
by MSATERM:2;
suppose
u . {} in [: the carrier' of S,{ the carrier of S}:]
;
( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )then consider a,
b being
object such that A1:
(
a in the
carrier' of
S &
b in { the carrier of S} &
u . {} = [a,b] )
by ZFMISC_1:def 2;
reconsider a =
a as
OperSymbol of
S by A1;
b = the
carrier of
S
by A1, TARSKI:def 1;
then consider p being
ArgumentSeq of
Sym (
a,
X)
such that A2:
u = [a, the carrier of S] -tree p
by A1, MSATERM:10;
Free (
S,
X)
= FreeMSA X
by MSAFREE3:31;
then reconsider p =
p as
Element of
Args (
a,
(Free (S,X)))
by INSTALG1:1;
u = a -term p
by A2;
hence
( ex
s being
SortSymbol of
S ex
x being
Element of
X . s st
t = x -term or ex
o being
OperSymbol of
S ex
p being
Element of
Args (
o,
(Free (S,X))) st
t = o -term p )
;
verum end;